Instances on PUnit

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

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

Equations

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

@[simp]

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

@[simp]

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