Instances on PUnit

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

theorem PUnit.addCommGroup.proof_2 : ∀ (a : PUnit.{u_1 + 1} ), 0 + a = 0 + a

instance PUnit.addCommGroup : AddCommGroup PUnit.{u_1 + 1}

Equations

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

theorem PUnit.addCommGroup.proof_4 : ∀ (x : PUnit.{u_1 + 1} ), (fun (x : ℕ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) 0 x = (fun (x : ℕ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) 0 x

theorem PUnit.addCommGroup.proof_6 : ∀ (a b : PUnit.{u_1 + 1} ), a - b = a - b

theorem PUnit.addCommGroup.proof_3 : ∀ (a : PUnit.{u_1 + 1} ), a + 0 = a + 0

theorem PUnit.addCommGroup.proof_9 : ∀ (n : ℕ) (a : PUnit.{u_1 + 1} ), (fun (x : ℤ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) (Int.negSucc n) a = (fun (x : ℤ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) (Int.negSucc n) a

theorem PUnit.addCommGroup.proof_7 : ∀ (a : PUnit.{u_1 + 1} ), (fun (x : ℤ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) 0 a = (fun (x : ℤ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) 0 a

theorem PUnit.addCommGroup.proof_8 : ∀ (n : ℕ) (a : PUnit.{u_1 + 1} ), (fun (x : ℤ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) (Int.ofNat n.succ) a = (fun (x : ℤ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) (Int.ofNat n.succ) a

theorem PUnit.addCommGroup.proof_1 : ∀ (a b c : PUnit.{u_1 + 1} ), a + b + c = a + b + c

theorem PUnit.addCommGroup.proof_10 : ∀ (a : PUnit.{u_1 + 1} ), -a + a = -a + a

theorem PUnit.addCommGroup.proof_5 : ∀ (n : ℕ) (x : PUnit.{u_1 + 1} ), (fun (x : ℕ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) (n + 1) x = (fun (x : ℕ) (x : PUnit.{u_1 + 1} ) => PUnit.unit) (n + 1) x

theorem PUnit.addCommGroup.proof_11 : ∀ (a b : PUnit.{u_1 + 1} ), a + b = a + b

instance PUnit.commGroup : CommGroup PUnit.{u_1 + 1}

Equations

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

instance PUnit.instZero : Zero PUnit.{1}

Equations

• PUnit.instZero = { zero := () }

instance PUnit.instOne : One PUnit.{1}

Equations

• PUnit.instOne = { one := () }

instance PUnit.instAdd_mathlib : Add PUnit.{1}

Equations

• PUnit.instAdd_mathlib = { add := fun (x x : PUnit.{1}) => () }

instance PUnit.instMul_mathlib : Mul PUnit.{1}

Equations

• PUnit.instMul_mathlib = { mul := fun (x x : PUnit.{1}) => () }

instance PUnit.instSub_mathlib : Sub PUnit.{1}

Equations

• PUnit.instSub_mathlib = { sub := fun (x x : PUnit.{1}) => () }

instance PUnit.instDiv_mathlib : Div PUnit.{1}

Equations

• PUnit.instDiv_mathlib = { div := fun (x x : PUnit.{1}) => () }

instance PUnit.instNeg : Neg PUnit.{1}

Equations

• PUnit.instNeg = { neg := fun (x : PUnit.{1}) => () }

instance PUnit.instInv : Inv PUnit.{1}

Equations

• PUnit.instInv = { inv := fun (x : PUnit.{1}) => () }

@[simp]

theorem PUnit.zero_eq : 0 = PUnit.unit

@[simp]

theorem PUnit.one_eq : 1 = PUnit.unit

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance PUnit.commRing : CommRing PUnit.{u_1 + 1}

Equations

• PUnit.commRing = let __spread.0 := PUnit.commGroup; let __spread.1 := PUnit.addCommGroup; CommRing.mk ⋯

instance PUnit.cancelCommMonoidWithZero : CancelCommMonoidWithZero PUnit.{u_1 + 1}

Equations

• PUnit.cancelCommMonoidWithZero = CancelCommMonoidWithZero.mk

instance PUnit.normalizedGCDMonoid : NormalizedGCDMonoid PUnit.{u_1 + 1}

Equations

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

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

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

@[simp]

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

instance PUnit.canonicallyOrderedAddCommMonoid : CanonicallyOrderedAddCommMonoid PUnit.{u_1 + 1}

Equations

• PUnit.canonicallyOrderedAddCommMonoid = CanonicallyOrderedAddCommMonoid.mk @PUnit.canonicallyOrderedAddCommMonoid.proof_1 ⋯

instance PUnit.linearOrderedCancelAddCommMonoid : LinearOrderedCancelAddCommMonoid PUnit.{u_1 + 1}

Equations

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

instance PUnit.instLinearOrderedAddCommMonoidWithTop : LinearOrderedAddCommMonoidWithTop PUnit.{u_1 + 1}

Equations

• PUnit.instLinearOrderedAddCommMonoidWithTop = LinearOrderedAddCommMonoidWithTop.mk PUnit.instLinearOrderedAddCommMonoidWithTop.proof_1

instance PUnit.vadd {R : Type u_1} : VAdd R PUnit.{u_3 + 1}

Equations

• PUnit.vadd = { vadd := fun (x : R) (x : PUnit.{?u.2 + 1} ) => PUnit.unit }

instance PUnit.smul {R : Type u_1} : SMul R PUnit.{u_3 + 1}

Equations

• PUnit.smul = { smul := fun (x : R) (x : PUnit.{?u.2 + 1} ) => PUnit.unit }

@[simp]

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

@[simp]

theorem PUnit.smul_eq {R : Type u_3} (y : PUnit.{u_4 + 1} ) (r : R) : r • y = PUnit.unit

instance PUnit.instIsCentralVAdd {R : Type u_1} : IsCentralVAdd R PUnit.{u_3 + 1}

Equations

• ⋯ = ⋯

instance PUnit.instIsCentralScalar {R : Type u_1} : IsCentralScalar R PUnit.{u_3 + 1}

Equations

• ⋯ = ⋯

instance PUnit.instVAddCommClass {R : Type u_1} {S : Type u_2} : VAddCommClass R S PUnit.{u_3 + 1}

Equations

• ⋯ = ⋯

instance PUnit.instSMulCommClass {R : Type u_1} {S : Type u_2} : SMulCommClass R S PUnit.{u_3 + 1}

Equations

• ⋯ = ⋯

instance PUnit.instIsScalarTowerOfVAdd {R : Type u_1} {S : Type u_2} [VAdd R S] : VAddAssocClass R S PUnit.{u_3 + 1}

Equations

• ⋯ = ⋯

instance PUnit.instIsScalarTowerOfSMul {R : Type u_1} {S : Type u_2} [SMul R S] : IsScalarTower R S PUnit.{u_3 + 1}

Equations

• ⋯ = ⋯

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

Equations

• PUnit.smulWithZero = let __spread.0 := PUnit.smul; SMulWithZero.mk ⋯

instance PUnit.mulAction {R : Type u_1} [Monoid R] : MulAction R PUnit.{u_3 + 1}

Equations

• PUnit.mulAction = let __spread.0 := PUnit.smul; MulAction.mk ⋯ ⋯

instance PUnit.distribMulAction {R : Type u_1} [Monoid R] : DistribMulAction R PUnit.{u_3 + 1}

Equations

• PUnit.distribMulAction = let __spread.0 := PUnit.mulAction; DistribMulAction.mk ⋯ ⋯

instance PUnit.mulDistribMulAction {R : Type u_1} [Monoid R] : MulDistribMulAction R PUnit.{u_3 + 1}

Equations

• PUnit.mulDistribMulAction = let __spread.0 := PUnit.mulAction; MulDistribMulAction.mk ⋯ ⋯

instance PUnit.mulSemiringAction {R : Type u_1} [Semiring R] : MulSemiringAction R PUnit.{u_3 + 1}

Equations

• PUnit.mulSemiringAction = let __src := PUnit.distribMulAction; let __src_1 := PUnit.mulDistribMulAction; MulSemiringAction.mk ⋯ ⋯

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

Equations

• PUnit.mulActionWithZero = let __src := PUnit.mulAction; let __src_1 := PUnit.smulWithZero; MulActionWithZero.mk ⋯ ⋯

instance PUnit.module {R : Type u_1} [Semiring R] : Module R PUnit.{u_3 + 1}

Equations

• PUnit.module = let __spread.0 := PUnit.distribMulAction; Module.mk ⋯ ⋯