Commit 2023-07-29 12:41 cd76c193

View on Github →

feat: groups with zero with a smooth division away from zero (#6069) We have currently (additive or multiplicative) Lie groups but no typeclass to express that division is smooth away from zero in fields. This PR adds such a typeclass, modelled on the one we already have in topological spaces.

Estimated changes

added theorem ContMDiff.div₀
added theorem ContMDiff.inv₀
added theorem ContMDiffAt.div₀
added theorem ContMDiffAt.inv₀
added theorem ContMDiffOn.div₀
added theorem ContMDiffOn.inv₀
added theorem Smooth.div₀
added theorem Smooth.inv₀
added theorem SmoothAt.div₀
added theorem SmoothAt.inv₀
added theorem SmoothOn.div₀
added theorem SmoothOn.inv₀
added theorem SmoothOn_inv₀
added theorem SmoothWithinAt.div₀
added theorem SmoothWithinAt.inv₀
added theorem smoothAt_inv₀
added theorem ContMDiff.div_const
added theorem ContMDiffOn.div_const
modified theorem Smooth.contMDiff
modified theorem SmoothAt.contMDiffAt
modified theorem SmoothOn.contMDiffOn