Commit 2021-07-07 15:54 e0ca8534

View on Github →

feat(algebra/group/units): teach simps about units (#8204) This also introduces units.copy to match invertible.copy, and uses it to make some lemmas in normed_space/units true by rfl (and generated by simps).

Estimated changes

Modified src/algebra/group/units.lean

added def units.copy

added theorem units.copy_eq

added def units.simps.coe

added def units.simps.coe_inv

Modified src/algebra/invertible.lean

deleted theorem unit_of_invertible_inv

deleted theorem unit_of_invertible_val

Modified src/algebra/lie/classical.lean

Modified src/analysis/normed_space/units.lean

deleted theorem units.add_coe

deleted theorem units.one_sub_coe

deleted theorem units.unit_of_nearby_coe