Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-19 17:15 6f3e0ad1

View on Github →

feat(ring_theory/multiplicity): Multiplicity with units (#6729) Renames multiplicity.multiplicity_unit into multiplicity.is_unit_left. Adds :

  • multiplicity.is_unit_right
  • multiplicity.unit_left
  • multiplicity.unit_right

Estimated changes

modified theorem multiplicity.one_left
modified theorem multiplicity.one_right
added theorem multiplicity.unit_left