Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-17 21:08 9ff5e8d7

View on Github →

feat(algebra/punit_instances): punit instances (#828)

Estimated changes

added theorem punit.Inf_eq
added theorem punit.Sup_eq
added theorem punit.add_eq
added theorem punit.bot_eq
added theorem punit.inf_eq
added theorem punit.inv_eq
added theorem punit.mul_eq
added theorem punit.neg_eq
added theorem punit.not_lt
added theorem punit.one_eq
added theorem punit.smul_eq
added theorem punit.sup_eq
added theorem punit.top_eq
added theorem punit.zero_eq