Def Mathlib.Meta.Positivity.Meta.Positivity.solve

Modification history

2023-08-27 01:38

Mathlib/Tactic/Positivity/Core.lean

field_simp: Use positivity as a discharger (#6312) …

Added Mathlib.Meta.Positivity.Meta.Positivity.solve View on Github →