Def Mathlib.Tactic.LinearCombination.Ineq.mulConstRelData

Modification history

2024-11-11 01:53

Mathlib/Tactic/LinearCombination/Lemmas.lean

feat: extend `linear_combination` to prove inequalities (#16841) …

Added Mathlib.Tactic.LinearCombination.Ineq.mulConstRelData View on Github →