Commit 2024-10-21 14:11 f4c1fd55

View on Github →

feat: a ^ n = 1 ↔ n = 0 and similar (#17745) This PR adds a few lemmas about GroupsWithZero, more precisely:

  • the lemmas zero_pow_eq_one₀, zero_zpow_eq_one₀ to Algebra.GroupWithZero.Basic and
  • zpow_le_zpow_iff_right_of_lt_one₀, zpow_lt_zpow_iff_right_of_lt_one₀ and zpow_eq_one_iff_right₀ to Algebra.Order.GroupWithZero.Unbundled. Used in project Formalization of the Bruhat-Tits Tree.

Estimated changes

added theorem zero_pow_eq_one₀
added theorem zero_zpow_eq_one₀