Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-19 11:05 85636950

View on Github →

refactor(algebra/associated): move is_unit def to algebra/group (#2015)

  • refactor(algebra/associated): move is_unit def to algebra/group I think it makes sense to have it near units.
  • Add a docstring to units, mention is_unit there.

Estimated changes

deleted theorem is_unit.map'
deleted theorem is_unit.map
deleted def is_unit
deleted theorem is_unit_iff_exists_inv'
deleted theorem is_unit_iff_exists_inv
deleted theorem is_unit_nat
deleted theorem is_unit_of_mul_one
deleted theorem is_unit_one
deleted theorem is_unit_unit
deleted theorem units.is_unit_mul_units
added theorem is_unit.map'
added theorem is_unit.map
added def is_unit
added theorem is_unit_iff_exists_inv
added theorem is_unit_nat
added theorem is_unit_of_mul_one
added theorem is_unit_one
added theorem is_unit_unit