Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-06 16:31 0a7ff10f

View on Github →

feat(algebra/units): some norm_cast attributes (#2612)

Estimated changes

Modified src/algebra/group/units.lean

modified theorem units.coe_inv

modified theorem units.coe_mul

modified theorem units.coe_one

Modified src/algebra/group_power.lean

modified theorem units.coe_pow

Modified src/group_theory/subgroup.lean

modified theorem is_add_subgroup.gsmul_coe

modified theorem is_subgroup.coe_gpow

Modified src/group_theory/submonoid.lean

modified theorem is_add_submonoid.smul_coe

modified theorem is_submonoid.coe_pow