Instances on PUnit

This file collects facts about algebraic structures on the one-element type, e.g. that it is a commutative ring.

ink

def PUnit.addCommGroup.proof_4 : ∀ (x : PUnit), (fun x x => PUnit.unit) 0 x = (fun x x => PUnit.unit) 0 x

Equations

• (_ : (fun x x => PUnit.unit) 0 x = (fun x x => PUnit.unit) 0 x) = (_ : (fun x x => PUnit.unit) 0 x = (fun x x => PUnit.unit) 0 x)

ink

def PUnit.addCommGroup.proof_1 : ∀ (a b c : PUnit), a + b + c = a + b + c

Equations

• (_ : a + b + c = a + b + c) = (_ : a + b + c = a + b + c)

ink

def PUnit.addCommGroup.proof_2 : ∀ (a : PUnit), 0 + a = 0 + a

Equations

• (_ : 0 + a = 0 + a) = (_ : 0 + a = 0 + a)

ink

instance PUnit.addCommGroup : AddCommGroup PUnit

Equations

• PUnit.addCommGroup = AddCommGroup.mk PUnit.addCommGroup.proof_11

ink

def PUnit.addCommGroup.proof_3 : ∀ (a : PUnit), a + 0 = a + 0

Equations

• (_ : a + 0 = a + 0) = (_ : a + 0 = a + 0)

ink

def PUnit.addCommGroup.proof_6 : ∀ (a b : PUnit), a - b = a - b

Equations

• (_ : a - b = a - b) = (_ : a - b = a - b)

ink

def PUnit.addCommGroup.proof_8 : ∀ (n : ℕ) (a : PUnit), (fun x x => PUnit.unit) (Int.ofNat (Nat.succ n)) a = (fun x x => PUnit.unit) (Int.ofNat (Nat.succ n)) a

Equations

• One or more equations did not get rendered due to their size.

ink

def PUnit.addCommGroup.proof_10 : ∀ (a : PUnit), -a + a = -a + a

Equations

• (_ : -a + a = -a + a) = (_ : -a + a = -a + a)

ink

def PUnit.addCommGroup.proof_9 : ∀ (n : ℕ) (a : PUnit), (fun x x => PUnit.unit) (Int.negSucc n) a = (fun x x => PUnit.unit) (Int.negSucc n) a

Equations

• (_ : (fun x x => PUnit.unit) (Int.negSucc n) a = (fun x x => PUnit.unit) (Int.negSucc n) a) = (_ : (fun x x => PUnit.unit) (Int.negSucc n) a = (fun x x => PUnit.unit) (Int.negSucc n) a)

ink

def PUnit.addCommGroup.proof_5 : ∀ (n : ℕ) (x : PUnit), (fun x x => PUnit.unit) (n + 1) x = (fun x x => PUnit.unit) (n + 1) x

Equations

• (_ : (fun x x => PUnit.unit) (n + 1) x = (fun x x => PUnit.unit) (n + 1) x) = (_ : (fun x x => PUnit.unit) (n + 1) x = (fun x x => PUnit.unit) (n + 1) x)

ink

def PUnit.addCommGroup.proof_7 : ∀ (a : PUnit), (fun x x => PUnit.unit) 0 a = (fun x x => PUnit.unit) 0 a

Equations

• (_ : (fun x x => PUnit.unit) 0 a = (fun x x => PUnit.unit) 0 a) = (_ : (fun x x => PUnit.unit) 0 a = (fun x x => PUnit.unit) 0 a)

ink

def PUnit.addCommGroup.proof_11 : ∀ (a b : PUnit), a + b = a + b

Equations

• (_ : a + b = a + b) = (_ : a + b = a + b)

ink

instance PUnit.commGroup : CommGroup PUnit

Equations

• PUnit.commGroup = CommGroup.mk PUnit.commGroup.proof_11

ink

@[simp]

theorem PUnit.zero_eq : 0 = PUnit.unit

ink

@[simp]

theorem PUnit.one_eq : 1 = PUnit.unit

ink

@[simp]

theorem PUnit.add_eq {x : PUnit} {y : PUnit} : x + y = PUnit.unit

ink

@[simp]

theorem PUnit.mul_eq {x : PUnit} {y : PUnit} : x * y = PUnit.unit

ink

@[simp]

theorem PUnit.sub_eq {x : PUnit} {y : PUnit} : x - y = PUnit.unit

ink

@[simp]

theorem PUnit.div_eq {x : PUnit} {y : PUnit} : x / y = PUnit.unit

ink

@[simp]

theorem PUnit.neg_eq {x : PUnit} : -x = PUnit.unit

ink

@[simp]

theorem PUnit.inv_eq {x : PUnit} : x⁻¹ = PUnit.unit

ink

instance PUnit.commRing : CommRing PUnit

Equations

• PUnit.commRing = let src := PUnit.commGroup; let src_1 := PUnit.addCommGroup; CommRing.mk (_ : ∀ (a b : PUnit), a * b = b * a)

ink

instance PUnit.cancelCommMonoidWithZero : CancelCommMonoidWithZero PUnit

Equations

• PUnit.cancelCommMonoidWithZero = let src := PUnit.commRing; CancelCommMonoidWithZero.mk

ink

instance PUnit.normalizedGCDMonoid : NormalizedGCDMonoid PUnit

Equations

• PUnit.normalizedGCDMonoid = NormalizedGCDMonoid.mk PUnit.normalizedGCDMonoid.proof_10 PUnit.normalizedGCDMonoid.proof_11

ink

theorem PUnit.gcd_eq {x : PUnit} {y : PUnit} : gcd x y = PUnit.unit

ink

theorem PUnit.lcm_eq {x : PUnit} {y : PUnit} : lcm x y = PUnit.unit

ink

@[simp]

theorem PUnit.norm_unit_eq {x : PUnit} : normUnit x = 1

ink

instance PUnit.canonicallyOrderedAddMonoid : CanonicallyOrderedAddMonoid PUnit

Equations

• One or more equations did not get rendered due to their size.

ink

instance PUnit.linearOrderedCancelAddCommMonoid : LinearOrderedCancelAddCommMonoid PUnit

Equations

• One or more equations did not get rendered due to their size.

ink

instance PUnit.instLinearOrderedAddCommMonoidWithTopPUnit : LinearOrderedAddCommMonoidWithTop PUnit

Equations

• One or more equations did not get rendered due to their size.

ink

instance PUnit.vadd {R : Type u_1} : VAdd R PUnit

Equations

• PUnit.vadd = { vadd := fun x x => PUnit.unit }

ink

instance PUnit.smul {R : Type u_1} : SMul R PUnit

Equations

• PUnit.smul = { smul := fun x x => PUnit.unit }

ink

@[simp]

theorem PUnit.vadd_eq {R : Type u_1} (y : PUnit) (r : R) : r +ᵥ y = PUnit.unit

ink

@[simp]

theorem PUnit.smul_eq {R : Type u_1} (y : PUnit) (r : R) : r • y = PUnit.unit

ink

instance PUnit.instIsCentralVAddPUnitVaddAddOpposite {R : Type u_1} : IsCentralVAdd R PUnit

Equations

• @PUnit.instIsCentralVAddPUnitVaddAddOpposite = @PUnit.instIsCentralVAddPUnitVaddAddOpposite.proof_1

ink

def PUnit.instIsCentralVAddPUnitVaddAddOpposite.proof_1 {R : Type u_1} : IsCentralVAdd R PUnit

Equations

• (_ : IsCentralVAdd R PUnit) = (_ : IsCentralVAdd R PUnit)

ink

instance PUnit.instIsCentralScalarPUnitSmulMulOpposite {R : Type u_1} : IsCentralScalar R PUnit

Equations

• @PUnit.instIsCentralScalarPUnitSmulMulOpposite = @PUnit.instIsCentralScalarPUnitSmulMulOpposite.proof_1

ink

def PUnit.instVAddCommClassPUnitVaddVadd.proof_1 {R : Type u_1} {S : Type u_2} : VAddCommClass R S PUnit

Equations

• (_ : VAddCommClass R S PUnit) = (_ : VAddCommClass R S PUnit)

ink

instance PUnit.instVAddCommClassPUnitVaddVadd {R : Type u_1} {S : Type u_2} : VAddCommClass R S PUnit

Equations

• @PUnit.instVAddCommClassPUnitVaddVadd = @PUnit.instVAddCommClassPUnitVaddVadd.proof_1

ink

instance PUnit.instSMulCommClassPUnitSmulSmul {R : Type u_1} {S : Type u_2} : SMulCommClass R S PUnit

Equations

• @PUnit.instSMulCommClassPUnitSmulSmul = @PUnit.instSMulCommClassPUnitSmulSmul.proof_1

ink

instance PUnit.instIsScalarTowerPUnitVaddVadd {R : Type u_1} {S : Type u_2} [inst : VAdd R S] : VAddAssocClass R S PUnit

Equations

• @PUnit.instIsScalarTowerPUnitVaddVadd = @PUnit.instIsScalarTowerPUnitVaddVadd.proof_1

ink

def PUnit.instIsScalarTowerPUnitVaddVadd.proof_1 {R : Type u_1} {S : Type u_2} [inst : VAdd R S] : VAddAssocClass R S PUnit

Equations

• (_ : VAddAssocClass R S PUnit) = (_ : VAddAssocClass R S PUnit)

ink

instance PUnit.instIsScalarTowerPUnitSmulSmul {R : Type u_1} {S : Type u_2} [inst : SMul R S] : IsScalarTower R S PUnit

Equations

• @PUnit.instIsScalarTowerPUnitSmulSmul = @PUnit.instIsScalarTowerPUnitSmulSmul.proof_1

ink

instance PUnit.smulWithZero {R : Type u_1} [inst : Zero R] : SMulWithZero R PUnit

Equations

• PUnit.smulWithZero = let src := PUnit.smul; SMulWithZero.mk (_ : ∀ (m : PUnit), 0 • m = 0)

ink

instance PUnit.mulAction {R : Type u_1} [inst : Monoid R] : MulAction R PUnit

Equations

• PUnit.mulAction = let src := PUnit.smul; MulAction.mk (_ : ∀ (b : PUnit), 1 • b = b) (_ : ∀ (x y : R) (b : PUnit), (x * y) • b = x • y • b)

ink

instance PUnit.distribMulAction {R : Type u_1} [inst : Monoid R] : DistribMulAction R PUnit

Equations

• PUnit.distribMulAction = let src := PUnit.mulAction; DistribMulAction.mk (_ : ∀ (a : R), a • 0 = 0) (_ : ∀ (a : R) (x y : PUnit), a • (x + y) = a • x + a • y)

ink

instance PUnit.mulDistribMulAction {R : Type u_1} [inst : Monoid R] : MulDistribMulAction R PUnit

Equations

• PUnit.mulDistribMulAction = let src := PUnit.mulAction; MulDistribMulAction.mk (_ : ∀ (r : R) (x y : PUnit), r • (x * y) = r • x * r • y) (_ : ∀ (r : R), r • 1 = 1)

ink

instance PUnit.mulSemiringAction {R : Type u_1} [inst : Semiring R] : MulSemiringAction R PUnit

Equations

• One or more equations did not get rendered due to their size.

ink

instance PUnit.mulActionWithZero {R : Type u_1} [inst : MonoidWithZero R] : MulActionWithZero R PUnit

Equations

• PUnit.mulActionWithZero = let src := PUnit.mulAction; let src_1 := PUnit.smulWithZero; MulActionWithZero.mk (_ : ∀ (a : R), a • 0 = 0) (_ : ∀ (m : PUnit), 0 • m = 0)

ink

instance PUnit.module {R : Type u_1} [inst : Semiring R] : Module R PUnit

Equations

• PUnit.module = let src := PUnit.distribMulAction; Module.mk (_ : ∀ (r s : R) (x : PUnit), (r + s) • x = r • x + s • x) (_ : ∀ (x : PUnit), 0 • x = 0)