PUnit is a GCD monoid

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

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 y : PUnit.{u_1 + 1}} : gcd x y = unit

@[simp]

theorem PUnit.lcm_eq {x y : PUnit.{u_1 + 1}} : lcm x y = unit

@[simp]

theorem PUnit.norm_unit_eq {x : PUnit.{u_1 + 1}} : normUnit x = 1