Solutions_S03_Building_the_Gaussian_Integers.lean`

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Imports (3)

structure GaussInt line 6 source
no axioms what this means
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:6 (same declaration text).
instance GaussInt.(instance at line 12) line 12 source
instance GaussInt.(instance at line 15) line 15 source
instance GaussInt.(instance at line 18) line 18 source
instance GaussInt.(instance at line 21) line 21 source
instance GaussInt.(instance at line 24) line 24 source
theorem GaussInt.zero_def line 27 source
no axioms what this means
Statement uses: Eq, GaussInt, OfNat.ofNat, GaussInt.mk, Int
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:27 (same declaration text).
theorem GaussInt.one_def line 30 source
no axioms what this means
Statement uses: Eq, GaussInt, OfNat.ofNat, GaussInt.mk, Int
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:30 (same declaration text).
theorem GaussInt.add_def line 33 source
no axioms what this means
Statement uses: GaussInt, Eq, HAdd.hAdd, GaussInt.mk, Int, GaussInt.re, GaussInt.im
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:33 (same declaration text).
theorem GaussInt.neg_def line 36 source
no axioms what this means
Statement uses: GaussInt, Eq, Neg.neg, GaussInt.mk, Int, GaussInt.re, GaussInt.im
Proof uses: rfl
3 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:36 (same declaration text).
theorem GaussInt.mul_def line 39 source
no axioms what this means
Statement uses: GaussInt, Eq, HMul.hMul, GaussInt.mk, HSub.hSub, Int, GaussInt.re, GaussInt.im, HAdd.hAdd
Proof uses: rfl
9 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:39 (same declaration text).
theorem GaussInt.zero_re line 44 source
no axioms what this means
Statement uses: Eq, Int, GaussInt.re, OfNat.ofNat, GaussInt
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:44 (same declaration text).
theorem GaussInt.zero_im line 48 source
no axioms what this means
Statement uses: Eq, Int, GaussInt.im, OfNat.ofNat, GaussInt
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:48 (same declaration text).
theorem GaussInt.one_re line 52 source
no axioms what this means
Statement uses: Eq, Int, GaussInt.re, OfNat.ofNat, GaussInt
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:52 (same declaration text).
theorem GaussInt.one_im line 56 source
no axioms what this means
Statement uses: Eq, Int, GaussInt.im, OfNat.ofNat, GaussInt
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:56 (same declaration text).
theorem GaussInt.add_re line 60 source
no axioms what this means
Statement uses: GaussInt, Eq, Int, GaussInt.re, HAdd.hAdd
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:60 (same declaration text).
theorem GaussInt.add_im line 64 source
no axioms what this means
Statement uses: GaussInt, Eq, Int, GaussInt.im, HAdd.hAdd
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:64 (same declaration text).
theorem GaussInt.neg_re line 68 source
no axioms what this means
Statement uses: GaussInt, Eq, Int, GaussInt.re, Neg.neg
Proof uses: rfl
3 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:68 (same declaration text).
theorem GaussInt.neg_im line 72 source
no axioms what this means
Statement uses: GaussInt, Eq, Int, GaussInt.im, Neg.neg
Proof uses: rfl
3 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:72 (same declaration text).
theorem GaussInt.mul_re line 76 source
no axioms what this means
Statement uses: GaussInt, Eq, Int, GaussInt.re, HMul.hMul, HSub.hSub, GaussInt.im
Proof uses: rfl
7 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:76 (same declaration text).
theorem GaussInt.mul_im line 80 source
no axioms what this means
Statement uses: GaussInt, Eq, Int, GaussInt.im, HMul.hMul, HAdd.hAdd, GaussInt.re
Proof uses: rfl
7 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:80 (same declaration text).
instance GaussInt.instCommRing line 83 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, GaussInt
Proof uses: CommRing.mk, Ring.mk, Semiring.mk, AddCommMonoid.mk, AddMonoid.mk, AddSemigroup.mk, Add.mk, HAdd.hAdd, Zero.mk, OfNat.ofNat, nsmulRec, Monoid.mk, Semigroup.mk, Mul.mk, HMul.hMul, One.mk, npowRecAuto, NatCast.mk, Nat.unaryCast, Neg.mk and 6 more
34 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:83 (same declaration text).
Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
theorem GaussInt.sub_re line 132 source
standard axioms: Quot.sound, propext what this means
Statement uses: GaussInt, Eq, Int, GaussInt.re, HSub.hSub
Proof uses: rfl
15 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:132 (same declaration text).
theorem GaussInt.sub_im line 136 source
standard axioms: Quot.sound, propext what this means
Statement uses: GaussInt, Eq, Int, GaussInt.im, HSub.hSub
Proof uses: rfl
15 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:136 (same declaration text).
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
instance GaussInt.(instance at line 139) line 139 source
def Int.div' line 148 source
no axioms what this means
Statement uses: Int
Proof uses: HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:157 (same declaration text).
def Int.mod' line 151 source
no axioms what this means
Statement uses: Int
Proof uses: HSub.hSub, HMod.hMod, HAdd.hAdd, HDiv.hDiv, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:160 (same declaration text).
theorem Int.div'_add_mod' line 154 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, HAdd.hAdd, HMul.hMul, Int.div', Int.mod'
Proof uses: Eq.mpr, HDiv.hDiv, OfNat.ofNat, id, congrArg, Int.div'.eq_1, HSub.hSub, HMod.hMod, Int.mod'.eq_1, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat, Nat.rawCast and 52 more
71 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:163 (same declaration text).
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Int.abs_mod'_le line 158 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, LT.lt, OfNat.ofNat, LE.le, abs, Int.mod', HDiv.hDiv
Proof uses: Eq.mpr, HSub.hSub, HMod.hMod, HAdd.hAdd, id, Eq, congrArg, Int.mod'.eq_1, And, Neg.neg, propext, abs_le, And.intro, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow and 59 more
86 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:167 (same declaration text).
Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Int.mod'_eq line 167 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, Int.mod', HSub.hSub, HMul.hMul, Int.div'
Proof uses: Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, OfNat.ofNat, Eq.mp, HAdd.hAdd, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.neg_congr and 48 more
67 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:176 (same declaration text).
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem aux line 171 source
Distinct definitions of this name: MIL/C11_Topology/S03_Topological_Spaces.lean:102 (different declaration text), MIL/C11_Topology/solutions/Solutions_S03_Topological_Spaces.lean:106 (different declaration text). Qualify references as aux@path.
theorem sq_add_sq_eq_zero line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, LinearOrder, IsStrictOrderedRing, Iff, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, And
Proof uses: Iff.intro, And.intro, Eq.mp, congrArg, add_comm, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_add, Eq.refl, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.zero_natPow, Eq.symm
46 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:180 (same statement text; different proof or body). Qualify references as sq_add_sq_eq_zero@path.
Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def GaussInt.norm line 191 source
standard axioms: propext what this means
Statement uses: GaussInt, Int
Proof uses: HAdd.hAdd, HPow.hPow, Nat, GaussInt.re, OfNat.ofNat, GaussInt.im
6 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:185 (same declaration text).
theorem GaussInt.norm_nonneg line 195 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: GaussInt, LE.le, Int, OfNat.ofNat, GaussInt.norm
Proof uses: add_nonneg, HPow.hPow, Nat, GaussInt.re, GaussInt.im, sq_nonneg
27 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:189 (same statement text; different proof or body). Qualify references as GaussInt.norm_nonneg@path.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem GaussInt.norm_eq_zero line 199 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: GaussInt, Iff, Eq, Int, GaussInt.norm, OfNat.ofNat
Proof uses: Eq.mpr, HAdd.hAdd, HPow.hPow, Nat, GaussInt.re, GaussInt.im, id, congrArg, GaussInt.norm.eq_1, And, propext, sq_add_sq_eq_zero, GaussInt.ext_iff, Iff.rfl
21 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:191 (same statement text; different proof or body). Qualify references as GaussInt.norm_eq_zero@path.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem GaussInt.norm_pos line 203 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: GaussInt, Iff, LT.lt, Int, OfNat.ofNat, GaussInt.norm, Ne
Proof uses: Eq.mpr, And, LE.le, id, Eq, congrArg, propext, lt_iff_le_and_ne, ne_comm, Not, Ne.eq_1, GaussInt.norm_eq_zero, of_eq_true, Eq.trans, True, congrFun', true_and, iff_self
17 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:193 (same statement text; different proof or body). Qualify references as GaussInt.norm_pos@path.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem GaussInt.norm_mul line 207 source
standard axioms: Quot.sound, propext what this means
Statement uses: GaussInt, Eq, Int, GaussInt.norm, HMul.hMul
Proof uses: id, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HPow.hPow, Nat, HSub.hSub, GaussInt.re, GaussInt.im, OfNat.ofNat, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 50 more
37 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:195 (same statement text; different proof or body). Qualify references as GaussInt.norm_mul@path.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def GaussInt.conj line 211 source
no axioms what this means
Statement uses: GaussInt
Proof uses: GaussInt.mk, GaussInt.re, Neg.neg, Int, GaussInt.im
1 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:197 (same declaration text).
theorem GaussInt.conj_re line 215 source
no axioms what this means
Statement uses: GaussInt, Eq, Int, GaussInt.re, GaussInt.conj
Proof uses: rfl
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:201 (same declaration text).
theorem GaussInt.conj_im line 219 source
no axioms what this means
Statement uses: GaussInt, Eq, Int, GaussInt.im, GaussInt.conj, Neg.neg
Proof uses: rfl
1 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:205 (same declaration text).
theorem GaussInt.norm_conj line 222 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: GaussInt, Eq, Int, GaussInt.norm, GaussInt.conj
Proof uses: of_eq_true, HAdd.hAdd, HPow.hPow, Nat, GaussInt.re, OfNat.ofNat, GaussInt.im, Eq.trans, True, congrFun', congrArg, Even.neg_pow, Even, eq_self
21 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:208 (same declaration text).
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
instance GaussInt.(instance at line 224) line 224 source
instance GaussInt.(instance at line 227) line 227 source
theorem GaussInt.div_def line 230 source
standard axioms: propext what this means
Statement uses: GaussInt, Eq, HDiv.hDiv, GaussInt.mk, Int.div', GaussInt.re, HMul.hMul, GaussInt.conj, GaussInt.norm, GaussInt.im
Proof uses: rfl
6 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:216 (same declaration text).
theorem GaussInt.mod_def line 234 source
standard axioms: Quot.sound, propext what this means
Statement uses: GaussInt, Eq, HMod.hMod, HSub.hSub, HMul.hMul, HDiv.hDiv
Proof uses: rfl
15 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:220 (same declaration text).
theorem GaussInt.norm_mod_lt line 237 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: GaussInt, Ne, OfNat.ofNat, LT.lt, Int, GaussInt.norm, HMod.hMod
Proof uses: Eq.mpr, id, Eq, congrArg, propext, GaussInt.norm_pos, Trans.trans, LE.le, HDiv.hDiv, le_of_mul_le_mul_right, HMul.hMul, HAdd.hAdd, HPow.hPow, Nat, abs, Int.mod', GaussInt.re, GaussInt.im, Neg.neg, GaussInt.conj and 96 more
109 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:223 (same declaration text).
Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
theorem GaussInt.coe_natAbs_norm line 256 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: GaussInt, Eq, Int, Int.natAbs, GaussInt.norm
Proof uses: Int.natAbs_of_nonneg, GaussInt.norm_nonneg
2 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:242 (same declaration text).
theorem GaussInt.natAbs_norm_mod_lt line 259 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: GaussInt, Ne, OfNat.ofNat, LT.lt, Nat, Int.natAbs, GaussInt.norm, HMod.hMod
Proof uses: Iff.mp, Int, Int.ofNat_lt, Eq.mpr, id, Eq, congr, congrArg, Eq.trans, abs, Int.natCast_natAbs, abs_of_nonneg, of_eq_true, LE.le, GaussInt.norm_mod_lt
19 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:245 (same declaration text).
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem GaussInt.not_norm_mul_left_lt_norm line 265 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: GaussInt, Ne, OfNat.ofNat, Not, LT.lt, Nat, Int.natAbs, GaussInt.norm, HMul.hMul
Proof uses: not_lt_of_ge, Eq.mpr, LE.le, Int, id, Eq, congrArg, GaussInt.norm_mul, Int.natAbs_mul, le_mul_of_one_le_right, Nat.zero_le, Iff.mp, Int.ofNat_le, GaussInt.coe_natAbs_norm, Int.add_one_le_of_lt, Iff.mpr, GaussInt.norm_pos
30 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean:251 (same declaration text).
Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
instance GaussInt.(instance at line 274) line 274 source
example GaussInt.(example at line 288) line 288 source