mfderiv): make `model_with_corners` implicit in `has_mfderiv_at.add`, `has_mfderiv_at.mul` etc. (#17675)

Commit

3 years ago

chore(geometry/manifold/mfderiv): make `model_with_corners` implicit in `has_mfderiv_at.add`, `has_mfderiv_at.mul` etc. (#17675) This is split from #13250 as requested by reviewers.

Author

CBirkbeck

Parents

31c458dc

mathlib 98cdae56 - chore(geometry/manifold/mfderiv): make `model_with_corners` implicit in `has_mfderiv_at.add`, `has_mfderiv_at.mul` etc. (#17675)

mathlib
98cdae56 - chore(geometry/manifold/mfderiv): make `model_with_corners` implicit in `has_mfderiv_at.add`, `has_mfderiv_at.mul` etc. (#17675)