Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-07 09:57 c2476223

View on Github →

feat(group_theory/group_action/units): simp lemma for scalar action of is_unit.unit h (#14006)

Estimated changes

added theorem units.smul_mk0
added theorem units.smul_is_unit