Commit 2025-07-12 14:51 cd11c28c

View on Github →

chore(Units): better follow the naming convention (#26251) Moves

  • Units.ext -> Units.val_injective
  • Units.eq_iff -> Units.val_inj

Estimated changes

deleted theorem Units.eq_iff
modified theorem Units.ext
modified theorem Units.val_eq_one
added theorem Units.val_inj
added theorem Units.val_injective
modified theorem Units.coeHom_injective