mathlib3
a16650c4 - feat(geometry/manifold/algebra/smooth_functions): add `coe_fn_(linear_map|ring_hom|alg_hom)` (#7749)

Commit
4 years ago
feat(geometry/manifold/algebra/smooth_functions): add `coe_fn_(linear_map|ring_hom|alg_hom)` (#7749) Changed names to be consistent with the topology library and proven that some coercions are morphisms.
Author
Parents
Loading