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_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_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_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_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
Equations
- PUnit.instAdd_mathlib = { add := fun (x x : PUnit.{1}) => () }
Equations
- PUnit.instMul_mathlib = { mul := fun (x x : PUnit.{1}) => () }
Equations
- PUnit.instSub_mathlib = { sub := fun (x x : PUnit.{1}) => () }
Equations
- PUnit.instDiv_mathlib = { div := fun (x x : PUnit.{1}) => () }
Equations
- PUnit.instNeg = { neg := fun (x : PUnit.{1}) => () }
Equations
- PUnit.instInv = { inv := fun (x : PUnit.{1}) => () }
Equations
- PUnit.cancelCommMonoidWithZero = CancelCommMonoidWithZero.mk