Theorem Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg

Modification history

2026-01-23 08:59
Mathlib/Algebra/Order/Field/Basic.lean
refactor(Algebra/Order/Field/Basic): generalize file from `LinearOrder` to `PartialOrder` and `PosMulReflectLT` (#33100) …
Modified Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonnegView on Github →
2026-01-05 17:02
Mathlib/Algebra/Order/Field/Basic.lean
chore(positivity): make tactic lemmas public (#33593) …
Added Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonnegView on Github →