Commit 2023-01-09 20:40 39a53f6e

View on Github →

feat: Port algebra.punit_instances (#1319) Port of algebra.punit_instances

depends on: #1330
depends on: #1314

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/PUnitInstances.lean

added theorem PUnit.div_eq

added theorem PUnit.gcd_eq

added theorem PUnit.inv_eq

added theorem PUnit.lcm_eq

added theorem PUnit.mul_eq

added theorem PUnit.norm_unit_eq

added theorem PUnit.one_eq

added theorem PUnit.smul_eq

Modified Mathlib/Order/Basic.lean

Modified Mathlib/Order/CompleteBooleanAlgebra.lean

Modified Mathlib/Order/Heyting/Basic.lean