Commit 2026-03-14 20:09 5a2fd495

View on Github →

feat(Algebra/Module/Submodule): Add pointwise negation lemma (#36634)

  • Add Submodule.neg_eq_iff_neg_le proving -S = S ↔ -S ≤ S
  • Make arguments of Submodule.neg_le_neg and Submodule.neg_le implicit For completeness I added the set version:
  • Add Set.inv_eq_iff_inv_subset proving s⁻¹ = s ↔ s⁻¹ ⊆ s and its additive version I did not manage to give a short proof of the submodule version from the set version like it is the case for neg_le and neg_le_neg.

Estimated changes

modified theorem Submodule.neg_le
modified theorem Submodule.neg_le_neg