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.

def PUnit.addCommGroup.proof_4 :
∀ (x : PUnit), (fun x x => PUnit.unit) 0 x = (fun x x => PUnit.unit) 0 x
Equations
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)
def PUnit.addCommGroup.proof_2 :
∀ (a : PUnit), 0 + a = 0 + a
Equations
  • (_ : 0 + a = 0 + a) = (_ : 0 + a = 0 + a)
def PUnit.addCommGroup.proof_3 :
∀ (a : PUnit), a + 0 = a + 0
Equations
  • (_ : a + 0 = a + 0) = (_ : a + 0 = a + 0)
def PUnit.addCommGroup.proof_6 :
∀ (a b : PUnit), a - b = a - b
Equations
  • (_ : a - b = a - b) = (_ : a - b = a - b)
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.
def PUnit.addCommGroup.proof_10 :
∀ (a : PUnit), -a + a = -a + a
Equations
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
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
def PUnit.addCommGroup.proof_7 :
∀ (a : PUnit), (fun x x => PUnit.unit) 0 a = (fun x x => PUnit.unit) 0 a
Equations
def PUnit.addCommGroup.proof_11 :
∀ (a b : PUnit), a + b = a + b
Equations
  • (_ : a + b = a + b) = (_ : a + b = a + b)
@[simp]
theorem PUnit.add_eq {x : PUnit} {y : PUnit} :
@[simp]
theorem PUnit.mul_eq {x : PUnit} {y : PUnit} :
@[simp]
theorem PUnit.sub_eq {x : PUnit} {y : PUnit} :
@[simp]
theorem PUnit.div_eq {x : PUnit} {y : PUnit} :
@[simp]
theorem PUnit.neg_eq {x : PUnit} :
@[simp]
Equations
theorem PUnit.gcd_eq {x : PUnit} {y : PUnit} :
theorem PUnit.lcm_eq {x : PUnit} {y : PUnit} :
@[simp]
theorem PUnit.norm_unit_eq {x : PUnit} :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
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_1} (y : PUnit) (r : R) :
@[simp]
theorem PUnit.smul_eq {R : Type u_1} (y : PUnit) (r : R) :
instance PUnit.smulWithZero {R : Type u_1} [inst : Zero R] :
Equations
instance PUnit.mulAction {R : Type u_1} [inst : Monoid R] :
Equations
instance PUnit.distribMulAction {R : Type u_1} [inst : Monoid R] :
Equations
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • PUnit.mulActionWithZero = let src := PUnit.mulAction; let src_1 := PUnit.smulWithZero; MulActionWithZero.mk (_ : ∀ (a : R), a 0 = 0) (_ : ∀ (m : PUnit), 0 m = 0)
instance PUnit.module {R : Type u_1} [inst : Semiring R] :
Equations