Commit 2023-07-01 13:49 a9b3aae8

View on Github →

feat: port Geometry.Manifold.Algebra.SmoothFunctions (#5461)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/Algebra/SmoothFunctions.lean

added def SmoothMap.C

added def SmoothMap.coeFnAlgHom

added def SmoothMap.coeFnLinearMap

added def SmoothMap.coeFnMonoidHom

added def SmoothMap.coeFnRingHom

added theorem SmoothMap.coe_div

added theorem SmoothMap.coe_inv

added theorem SmoothMap.coe_mul

added theorem SmoothMap.coe_one

added theorem SmoothMap.coe_pow

added theorem SmoothMap.coe_smul

added def SmoothMap.compLeftMonoidHom

added def SmoothMap.compLeftRingHom

added def SmoothMap.evalRingHom

added theorem SmoothMap.mul_comp

added def SmoothMap.restrictMonoidHom

added def SmoothMap.restrictRingHom

added theorem SmoothMap.smul_comp'

added theorem SmoothMap.smul_comp