Inductive Mathlib.Meta.FunProp.DecompositionResult

Modification history

2026-05-29 12:25
Mathlib/Tactic/FunProp/FunctionData.lean
fix(Tactic/FunProp): detect `Continuous.subtype_mk` as compositional (#35683) …
Added Mathlib.Meta.FunProp.DecompositionResultView on Github →