Commit 2022-12-06 03:48 8a3baed4

View on Github →

feat: port Algebra.Group.WithOne.Defs (#841) mathlib3 commit hash e574b1a4e891376b0ef974b926da39e05da12a06

Estimated changes

added def WithOne.coe
added theorem WithOne.coe_inj
added theorem WithOne.coe_inv
added theorem WithOne.coe_mul
added theorem WithOne.coe_ne_one
added theorem WithOne.coe_unone
added theorem WithOne.one_ne_coe
added def WithOne.unone
added theorem WithOne.unone_coe
added def WithOne
added theorem WithZero.coe_div
added theorem WithZero.coe_inv
added theorem WithZero.coe_mul
added theorem WithZero.coe_one
added theorem WithZero.coe_pow
added theorem WithZero.coe_zpow
added theorem WithZero.inv_zero
added theorem WithZero.mul_zero
added theorem WithZero.zero_mul