Def Mathlib.Meta.FunProp.DecompositionResult.toTheoremForm

Modification history

2026-05-29 12:25

Mathlib/Tactic/FunProp/Theorems.lean

fix(Tactic/FunProp): detect `Continuous.subtype_mk` as compositional (#35683) …

Added Mathlib.Meta.FunProp.DecompositionResult.toTheoremForm View on Github →