Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-20 14:42 7e8432d4

View on Github →

chore(algebra/group_power/lemmas): Lemmas about gsmul (#8618) This restates some existing lemmas as monotone and strict_monotone, and provides new lemmas about the right argument of gsmul:

  • gsmul_le_gsmul'
  • gsmul_lt_gsmul'
  • gsmul_le_gsmul_iff'
  • gsmul_lt_gsmul_iff' This also removes an unnecessary linear_order assumption from gsmul_le_gsmul_iff and gsmul_lt_gsmul_iff.

Estimated changes

added theorem gsmul_eq_gsmul_iff'
added theorem gsmul_le_gsmul'
added theorem gsmul_le_gsmul_iff'
added theorem gsmul_lt_gsmul'
added theorem gsmul_lt_gsmul_iff'
added theorem gsmul_mono_left
added theorem gsmul_mono_right
added theorem gsmul_right_inj
added theorem gsmul_right_injective
added theorem gsmul_strict_mono_left