Commit 2026-11-10 11:56 4e74ccd9

View on Github →

chore(Algebra/GroupWithZero/Units/Basic): rename three lemmas ' -> ₀ (#43858) These lemmas about GroupWithZero are analogous to unprimed lemmas about groups. This PR renames them to use the usual convention of naming such lemmas with an underscored zero.

  • div_left_inj'
  • div_div_cancel_left'
  • div_div_div_cancel_left'

Estimated changes

deleted theorem div_div_cancel_left'
added theorem div_div_cancel_left₀
deleted theorem div_div_div_cancel_left'
deleted theorem div_left_inj'
added theorem div_left_inj₀