Solutions_S02_Algebraic_Structures.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)

structure C06S02.AddGroup₁ line 6 source
no axioms what this means
Distinct definitions of this name: MIL/C07_Structures/S02_Algebraic_Structures.lean:56 (same statement text; different proof or body). Qualify references as C06S02.AddGroup₁@path.
structure C06S02.Point line 16 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Also declared: MIL/C07_Structures/S02_Algebraic_Structures.lean:60 (same declaration text).
def C06S02.Point.add line 23 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: C06S02.Point
Proof uses: C06S02.Point.mk, HAdd.hAdd, Real, C06S02.Point.x, C06S02.Point.y, C06S02.Point.z
2 instances, coercions and auxiliary constants left out.
Also declared: MIL/C07_Structures/S02_Algebraic_Structures.lean:67 (same declaration text).
def C06S02.Point.neg line 26 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: C06S02.Point
Proof uses: C06S02.Point.mk, Neg.neg, Real, C06S02.Point.x, C06S02.Point.y, C06S02.Point.z
1 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C07_Structures/S02_Algebraic_Structures.lean:70 (same statement text; different proof or body). Qualify references as C06S02.Point.neg@path.
def C06S02.Point.zero line 29 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: C06S02.Point
Proof uses: C06S02.Point.mk, OfNat.ofNat, Real
2 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C07_Structures/S02_Algebraic_Structures.lean:72 (same statement text; different proof or body). Qualify references as C06S02.Point.zero@path.
def C06S02.Point.addGroupPoint line 32 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: C06S02.AddGroup₁, C06S02.Point
Proof uses: C06S02.AddGroup₁.mk, C06S02.Point.add, C06S02.Point.zero, C06S02.Point.neg
4 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C07_Structures/S02_Algebraic_Structures.lean:74 (same statement text; different proof or body). Qualify references as C06S02.Point.addGroupPoint@path.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
class C06S02.AddGroup₂ line 43 source
no axioms what this means
Distinct definitions of this name: MIL/C07_Structures/S02_Algebraic_Structures.lean:171 (same statement text; different proof or body). Qualify references as C06S02.AddGroup₂@path.
instance C06S02.hasAddAddGroup₂ line 52 source
no axioms what this means
Statement uses: C06S02.AddGroup₂, Add
Proof uses: Add.mk, C06S02.AddGroup₂.add
instance C06S02.hasZeroAddGroup₂ line 55 source
no axioms what this means
Statement uses: C06S02.AddGroup₂, Zero
Proof uses: Zero.mk, C06S02.AddGroup₂.zero
instance C06S02.hasNegAddGroup₂ line 58 source
no axioms what this means
Statement uses: C06S02.AddGroup₂, Neg
Proof uses: Neg.mk, C06S02.AddGroup₂.neg
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
instance C06S02.(instance at line 61) line 61 source