Mathlib v3 is deprecated. Go to Mathlib v4

Theorem units.val_eq_coe

Modification history

2021-08-09 13:47
src/algebra/group/units.lean
chore(algebra/group/units): Make coercion the simp-normal form of units (#8568) …
Added units.val_eq_coeView on Github →