Commit 2023-12-23 10:52 ea70e843

View on Github →

refactor: Deduplicate monotonicity of • lemmas (#9179) Remove the duplicates introduced in #8869 by sorting the lemmas in Algebra.Order.SMul into three files:

  • Algebra.Order.Module.Defs for the order isomorphism induced by scalar multiplication by a positivity element
  • Algebra.Order.Module.Pointwise for the order properties of scalar multiplication of sets. This file is new. I credit myself for https://github.com/leanprover-community/mathlib/pull/9078
  • Algebra.Order.Module.OrderedSMul: The material about OrderedSMul per se. Inherits the copyright header from Algebra.Order.SMul. This file should eventually be deleted. I move each #align to the correct file. On top of that, I delete unused redundant OrderedSMul instances (they were useful in Lean 3, but not anymore) and eq_of_smul_eq_smul_of_pos_of_le/eq_of_smul_eq_smul_of_neg_of_le since those lemmas are weird and unused.

Estimated changes

modified theorem smul_le_smul_of_nonneg_left
modified theorem smul_lt_smul_of_pos_left
modified theorem smul_lt_smul_of_pos_right
added theorem OrderedSMul.mk''
added theorem OrderedSMul.mk'
deleted theorem BddAbove.smul_of_nonneg
deleted theorem BddBelow.smul_of_nonneg
deleted def OrderIso.smulLeft
deleted theorem OrderedSMul.mk''
deleted theorem OrderedSMul.mk'
deleted theorem bddAbove_smul_iff_of_pos
deleted theorem bddBelow_smul_iff_of_pos
deleted theorem inv_smul_le_iff
deleted theorem inv_smul_lt_iff
deleted theorem le_inv_smul_iff
deleted theorem lowerBounds_smul_of_pos
deleted theorem lt_inv_smul_iff
deleted theorem monotone_smul_left
deleted theorem smul_le_smul_iff_of_pos
deleted theorem smul_le_smul_of_nonneg
deleted theorem smul_lt_smul_iff_of_pos
deleted theorem smul_lt_smul_of_pos
deleted theorem smul_max
deleted theorem smul_min
deleted theorem smul_pos_iff_of_pos
deleted theorem strictMono_smul_left
deleted theorem upperBounds_smul_of_pos
added theorem nnnorm_pos'
added def Equiv.smulRight