Commit 2025-06-18 15:21 d7c3d1e8

View on Github →

chore(Algebra/Order/Module/Defs): don't import fields (#25584) Instead move the few Field lemmas to a new file Algebra.Order.Module.Field (https://github.com/leanprover-community/mathlib3/pull/9077 for the copyright) and the positivity extension to Tactic.Positivity.Basic.

Estimated changes

deleted theorem inv_smul_le_iff_of_neg
deleted theorem inv_smul_lt_iff_of_neg
deleted theorem smul_inv_le_iff_of_neg
deleted theorem smul_inv_lt_iff_of_neg
added theorem inv_smul_le_iff_of_neg
added theorem inv_smul_lt_iff_of_neg
added theorem smul_inv_le_iff_of_neg
added theorem smul_inv_lt_iff_of_neg
modified theorem Nat.prod_factorial_pos