S03_Building_the_Gaussian_Integers.lean`

GitHub source file

53 declarations, 5 contain sorry, 0 declared as axioms

Imports (3)

Imported by 1 file

MIL.lean

structure GaussInt line 6 source
no axioms what this means
Also declared: MIL/C07_Structures/solutions/Solutions_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/solutions/Solutions_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/solutions/Solutions_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/solutions/Solutions_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/solutions/Solutions_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/solutions/Solutions_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/solutions/Solutions_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/solutions/Solutions_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/solutions/Solutions_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/solutions/Solutions_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/solutions/Solutions_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/solutions/Solutions_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/solutions/Solutions_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/solutions/Solutions_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/solutions/Solutions_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/solutions/Solutions_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/solutions/Solutions_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/solutions/Solutions_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/solutions/Solutions_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
example (example at line 146) line 146 source
example (example at line 149) line 149 source
example (example at line 152) line 152 source
def Int.div' line 157 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/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:148 (same declaration text).
def Int.mod' line 160 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/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:151 (same declaration text).
theorem Int.div'_add_mod' line 163 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/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:154 (same declaration text).
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Int.abs_mod'_le line 167 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/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:158 (same declaration text).
Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Int.mod'_eq line 176 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/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:167 (same declaration text).
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem sq_add_sq_eq_zero sorry line 180 source
depends on sorry what this means
Statement uses: Ring, LinearOrder, IsStrictOrderedRing, Iff, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, And
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C07_Structures/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:178 (same statement text; different proof or body). Qualify references as sq_add_sq_eq_zero@path.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def GaussInt.norm line 185 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/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:191 (same declaration text).
theorem GaussInt.norm_nonneg sorry line 189 source
depends on sorry what this means
Statement uses: GaussInt, LE.le, Int, OfNat.ofNat, GaussInt.norm
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
5 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C07_Structures/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:195 (same statement text; different proof or body). Qualify references as GaussInt.norm_nonneg@path.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem GaussInt.norm_eq_zero sorry line 191 source
depends on sorry what this means
Statement uses: GaussInt, Iff, Eq, Int, GaussInt.norm, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
7 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C07_Structures/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:199 (same statement text; different proof or body). Qualify references as GaussInt.norm_eq_zero@path.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem GaussInt.norm_pos sorry line 193 source
depends on sorry what this means
Statement uses: GaussInt, Iff, LT.lt, Int, OfNat.ofNat, GaussInt.norm, Ne
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
9 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C07_Structures/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:203 (same statement text; different proof or body). Qualify references as GaussInt.norm_pos@path.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem GaussInt.norm_mul sorry line 195 source
depends on sorry what this means
Statement uses: GaussInt, Eq, Int, GaussInt.norm, HMul.hMul
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
7 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C07_Structures/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:207 (same statement text; different proof or body). Qualify references as GaussInt.norm_mul@path.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def GaussInt.conj line 197 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/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:211 (same declaration text).
theorem GaussInt.conj_re line 201 source
no axioms what this means
Statement uses: GaussInt, Eq, Int, GaussInt.re, GaussInt.conj
Proof uses: rfl
Also declared: MIL/C07_Structures/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:215 (same declaration text).
theorem GaussInt.conj_im line 205 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/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:219 (same declaration text).
theorem GaussInt.norm_conj line 208 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/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:222 (same declaration text).
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
instance GaussInt.(instance at line 210) line 210 source
instance GaussInt.(instance at line 213) line 213 source
theorem GaussInt.div_def line 216 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/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:230 (same declaration text).
theorem GaussInt.mod_def line 220 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/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:234 (same declaration text).
theorem GaussInt.norm_mod_lt line 223 source
depends on sorry 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/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:237 (same declaration text).
Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
theorem GaussInt.coe_natAbs_norm line 242 source
depends on sorry 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/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:256 (same declaration text).
theorem GaussInt.natAbs_norm_mod_lt line 245 source
depends on sorry 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/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:259 (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 251 source
depends on sorry 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/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:265 (same declaration text).
Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
instance GaussInt.(instance at line 260) line 260 source
example GaussInt.(example at line 274) line 274 source