Theorem Mathlib.Meta.Positivity.smul_ne_zero_of_pos_of_ne_zero

Modification history

2026-01-05 17:02
Mathlib/Algebra/Order/Module/Field.lean
chore(positivity): make tactic lemmas public (#33593) …
Added Mathlib.Meta.Positivity.smul_ne_zero_of_pos_of_ne_zeroView on Github →