PFRPalomar/Solution.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem Marton.pfr_conjecture_aux line 25 source
2. theorem Marton.pfr_conjecture line 33 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: AddCommGroup, Eq, HSMul.hSMul, Nat, OfNat.ofNat, Set, Set.Finite, Set.Nonempty, Real, LE.le, Nat.card, HAdd.hAdd, HMul.hMul, Exists, AddSubgroup, And, LT.lt, HPow.hPow, Subtype, Membership.mem

   Proof uses: AddCommGroup.zmodModule

   64 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: PFRPalomar/Challenge.lean:69 (same statement text; different proof or body). Qualify references as Marton.pfr_conjecture@path.

   Tactic trace: 2 steps

   Open to load the checked before-and-after goal states.

3. theorem Marton.pfr_conjecture_nine_aux line 40 source
4. theorem Marton.pfr_conjecture_nine line 48 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: AddCommGroup, Eq, HSMul.hSMul, Nat, OfNat.ofNat, Set, Set.Finite, Set.Nonempty, Real, LE.le, Nat.card, HAdd.hAdd, HMul.hMul, Exists, AddSubgroup, And, LT.lt, HPow.hPow, Subtype, Membership.mem

   Proof uses: AddCommGroup.zmodModule

   64 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: PFRPalomar/Challenge.lean:84 (same statement text; different proof or body). Qualify references as Marton.pfr_conjecture_nine@path.

   Tactic trace: 2 steps

   Open to load the checked before-and-after goal states.

5. theorem Marton.torsion_pfr_conjecture line 55 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: AddCommGroup, Nat, LE.le, OfNat.ofNat, Eq, HSMul.hSMul, Set, Set.Finite, Set.Nonempty, Real, Nat.card, HAdd.hAdd, HMul.hMul, Exists, AddSubgroup, And, LT.lt, HPow.hPow, Subtype, Membership.mem

   Proof uses: Set.ncard, torsion_PFR, Exists.intro, And.intro

   78 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: PFRPalomar/Challenge.lean:98 (same statement text; different proof or body). Qualify references as Marton.torsion_pfr_conjecture@path.

   Tactic trace: 2 steps

   Open to load the checked before-and-after goal states.

6. theorem Marton.weak_pfr_int line 63 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: AddCommGroup, Module.Free, Int, Module.Finite, Set, Set.Finite, Set.Nonempty, Real, LE.le, Nat.card, HAdd.hAdd, HMul.hMul, Exists, And, HPow.hPow, Neg.neg, OfNat.ofNat, Nat, Module.finrank, Subtype and 5 more

   Proof uses: GE.ge, AffineSpace.finrank, weak_PFR_int_sumset, Exists.intro, And.intro

   68 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: PFRPalomar/Challenge.lean:114 (same statement text; different proof or body). Qualify references as Marton.weak_pfr_int@path.

   Tactic trace: 3 steps

   Open to load the checked before-and-after goal states.

7. theorem Marton.homomorphism_pfr_aux line 71 source
8. theorem Marton.homomorphism_pfr line 77 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: AddCommGroup, Finite, Eq, HSMul.hSMul, Nat, OfNat.ofNat, Set, Membership.mem, HSub.hSub, HAdd.hAdd, Exists, AddMonoidHom, And, LE.le, Nat.card, HPow.hPow

   Proof uses: AddCommGroup.zmodModule

   53 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: PFRPalomar/Challenge.lean:126 (same statement text; different proof or body). Qualify references as Marton.homomorphism_pfr@path.

   Tactic trace: 3 steps

   Open to load the checked before-and-after goal states.

9. theorem Marton.approx_hom_pfr_aux line 85 source
10. theorem Marton.approx_hom_pfr line 106 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: AddCommGroup, Finite, Eq, HSMul.hSMul, Nat, OfNat.ofNat, Real, LT.lt, LE.le, HPow.hPow, Nat.card, HMul.hMul, Prod, Set.ofPred, HAdd.hAdd, Prod.fst, Prod.snd, Exists, AddMonoidHom, HDiv.hDiv and 1 more

    Proof uses: AddCommGroup.zmodModule

    75 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: PFRPalomar/Challenge.lean:139 (same statement text; different proof or body). Qualify references as Marton.approx_hom_pfr@path.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.