Instances on PUnit #

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

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

∀ (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

source

theorem PUnit.addCommGroup.proof_2 :

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

source

instance PUnit.addCommGroup :

AddCommGroup PUnit.{u_1 + 1}

Equations

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

source

theorem PUnit.addCommGroup.proof_3 :

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

source

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

source

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

source

theorem PUnit.addCommGroup.proof_1 :

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

source

theorem PUnit.addCommGroup.proof_8 :

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

source

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

source

theorem PUnit.addCommGroup.proof_10 :

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

source

theorem PUnit.addCommGroup.proof_11 :

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

source

instance PUnit.commGroup :

CommGroup PUnit.{u_1 + 1}

Equations

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

source

instance PUnit.instZeroPUnit :

Zero PUnit.{1}

Equations

PUnit.instZeroPUnit = { zero := () }

source

instance PUnit.instOnePUnit :

One PUnit.{1}

Equations

PUnit.instOnePUnit = { one := () }

source

instance PUnit.instAddPUnit :

Add PUnit.{1}

Equations

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

source

instance PUnit.instMulPUnit :

Mul PUnit.{1}

Equations

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

source

instance PUnit.instSubPUnit :

Sub PUnit.{1}

Equations

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

source

instance PUnit.instDivPUnit :

Div PUnit.{1}

Equations

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

source

instance PUnit.instNegPUnit :

Neg PUnit.{1}

Equations

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

source

instance PUnit.instInvPUnit :

Inv PUnit.{1}

Equations

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

source

@[simp]

theorem PUnit.zero_eq :

0 = PUnit.unit

source

@[simp]

theorem PUnit.one_eq :

1 = PUnit.unit

source

theorem PUnit.add_eq {x : PUnit.{1}} {y : PUnit.{1}} :

x + y = PUnit.unit

source

theorem PUnit.mul_eq {x : PUnit.{1}} {y : PUnit.{1}} :

x * y = PUnit.unit

source

@[simp]

theorem PUnit.sub_eq {x : PUnit.{1}} {y : PUnit.{1}} :

x - y = PUnit.unit

source

@[simp]

theorem PUnit.div_eq {x : PUnit.{1}} {y : PUnit.{1}} :

x / y = PUnit.unit

source

@[simp]

theorem PUnit.neg_eq {x : PUnit.{1}} :

-x = PUnit.unit

source

@[simp]

theorem PUnit.inv_eq {x : PUnit.{1}} :

x⁻¹ = PUnit.unit

source

instance PUnit.commRing :

CommRing PUnit.{u_1 + 1}

Equations

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

source

instance PUnit.cancelCommMonoidWithZero :

CancelCommMonoidWithZero PUnit.{1}

Equations

PUnit.cancelCommMonoidWithZero = let __src := PUnit.commRing; CancelCommMonoidWithZero.mk

source

instance PUnit.normalizedGCDMonoid :

NormalizedGCDMonoid PUnit.{1}

Equations

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

source

theorem PUnit.gcd_eq {x : PUnit.{1}} {y : PUnit.{1}} :

gcd x y = PUnit.unit

source

theorem PUnit.lcm_eq {x : PUnit.{1}} {y : PUnit.{1}} :

lcm x y = PUnit.unit

source

@[simp]

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

normUnit x = 1

source

instance PUnit.canonicallyOrderedAddCommMonoid :

CanonicallyOrderedAddCommMonoid PUnit.{u_1 + 1}

Equations

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

source

instance PUnit.linearOrderedCancelAddCommMonoid :

LinearOrderedCancelAddCommMonoid PUnit.{u_1 + 1}

Equations

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

source

instance PUnit.instLinearOrderedAddCommMonoidWithTopPUnit :

LinearOrderedAddCommMonoidWithTop PUnit.{u_1 + 1}

Equations

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

source

instance PUnit.vadd {R : Type u_1} :

VAdd R PUnit.{u_3 + 1}

Equations

PUnit.vadd = { vadd := fun (x : R) (x : PUnit.{u_3 + 1} ) => PUnit.unit }

source

instance PUnit.smul {R : Type u_1} :

SMul R PUnit.{u_3 + 1}

Equations

PUnit.smul = { smul := fun (x : R) (x : PUnit.{u_3 + 1} ) => PUnit.unit }

source

@[simp]

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

r +ᵥ y = PUnit.unit

source

@[simp]

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

r • y = PUnit.unit

source

instance PUnit.instIsCentralVAddPUnitVaddAddOpposite {R : Type u_1} :

IsCentralVAdd R PUnit.{u_3 + 1}

Equations

⋯ = ⋯

source

instance PUnit.instIsCentralScalarPUnitSmulMulOpposite {R : Type u_1} :

IsCentralScalar R PUnit.{u_3 + 1}

Equations

⋯ = ⋯

source

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

VAddCommClass R S PUnit.{u_3 + 1}

Equations

⋯ = ⋯

source

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

SMulCommClass R S PUnit.{u_3 + 1}

Equations

⋯ = ⋯

source

instance PUnit.instIsScalarTowerOfVAdd {R : Type u_1} {S : Type u_2} [VAdd R S] :

VAddAssocClass R S PUnit.{u_3 + 1}

Equations

⋯ = ⋯

source

instance PUnit.instIsScalarTowerOfSMul {R : Type u_1} {S : Type u_2} [SMul R S] :

IsScalarTower R S PUnit.{u_3 + 1}

Equations

⋯ = ⋯

source

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

SMulWithZero R PUnit.{1}

Equations

PUnit.smulWithZero = let __src := PUnit.smul; SMulWithZero.mk ⋯

source

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

MulAction R PUnit.{u_3 + 1}

Equations

PUnit.mulAction = let __src := PUnit.smul; MulAction.mk ⋯ ⋯

source

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

DistribMulAction R PUnit.{u_3 + 1}

Equations

PUnit.distribMulAction = let __src := PUnit.mulAction; DistribMulAction.mk ⋯ ⋯

source

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

MulDistribMulAction R PUnit.{u_3 + 1}

Equations

PUnit.mulDistribMulAction = let __src := PUnit.mulAction; MulDistribMulAction.mk ⋯ ⋯

source

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 ⋯ ⋯

source

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 ⋯ ⋯

source

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

Module R PUnit.{u_3 + 1}

Equations

PUnit.module = let __src := PUnit.distribMulAction; Module.mk ⋯ ⋯

Documentation

Mathlib.Algebra.PUnitInstances

Instances on PUnit #