Documentation

Mathlib.Algebra.PUnitInstances

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_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_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_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
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
@[simp]
@[simp]
@[simp]
theorem PUnit.sub_eq {x : PUnit.{1}} {y : PUnit.{1}} :
@[simp]
theorem PUnit.div_eq {x : PUnit.{1}} {y : PUnit.{1}} :
@[simp]
Equations
Equations
  • One or more equations did not get rendered due to their size.
instance PUnit.vadd {R : Type u_1} :
Equations
instance PUnit.smul {R : Type u_1} :
Equations
@[simp]
theorem PUnit.vadd_eq {R : Type u_3} (y : PUnit.{u_4 + 1} ) (r : R) :
@[simp]
theorem PUnit.smul_eq {R : Type u_3} (y : PUnit.{u_4 + 1} ) (r : R) :
Equations
  • =
Equations
  • =
Equations
  • =
Equations
  • =
instance PUnit.instIsScalarTowerOfSMul {R : Type u_1} {S : Type u_2} [SMul R S] :
Equations
  • =
Equations
Equations
  • PUnit.mulAction = let __spread.0 := PUnit.smul; MulAction.mk
Equations
Equations
Equations
  • PUnit.mulSemiringAction = let __src := PUnit.distribMulAction; let __src_1 := PUnit.mulDistribMulAction; MulSemiringAction.mk
Equations
  • PUnit.mulActionWithZero = let __src := PUnit.mulAction; let __src_1 := PUnit.smulWithZero; MulActionWithZero.mk
instance PUnit.module {R : Type u_1} [Semiring R] :
Equations
  • PUnit.module = let __spread.0 := PUnit.distribMulAction; Module.mk