[Merged by Bors] - chore: missing fun_prop attribute#30635

sgouezel wants to merge 1 commit intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

sgouezel:SG_funprop12sgouezel/mathlib4:SG_funprop12Copy head branch name to clipboard