Commit 2026-01-15 15:56 d4fd214a

View on Github →

style: make fun_prop tests match the mathlib style guide better (#33999) Also add a very basic test about combining the unfolding and discharging behaviour.

Estimated changes

deleted def bar
deleted def foo
modified theorem prod_mk_Con
modified theorem prod_mk_Lin