Commit 2021-08-09 13:47 8196d4a2
View on Github →chore(algebra/group/units): Make coercion the simp-normal form of units (#8568)
It's already used as the output for @[simps]; this makes ↑u the simp-normal form of u.val and ↑(u⁻¹) the simp-normal form of u.inv.