Commit 2021-06-15 14:54 a16650c4

View on Github →

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.

Estimated changes

Modified src/geometry/manifold/algebra/smooth_functions.lean

modified def smooth_map.C

modified theorem smooth_map.coe_div

added def smooth_map.coe_fn_alg_hom

added def smooth_map.coe_fn_linear_map

added def smooth_map.coe_fn_monoid_hom

added def smooth_map.coe_fn_ring_hom

modified theorem smooth_map.coe_inv

modified theorem smooth_map.coe_smul

modified theorem smooth_map.smul_comp'

modified theorem smooth_map.smul_comp