Smooth structures #
In this file we define smooth structures that build on Lie groups. We prefer using the term smooth instead of Lie mainly because Lie ring has currently another use in mathematics.
- to_has_smooth_add : has_smooth_add I R
- smooth_mul : smooth (I.prod I) I (λ (p : R × R), (p.fst) * p.snd)
A smooth (semi)ring is a (semi)ring
R where addition and multiplication are smooth.
R is a ring, then negation is automatically smooth, as it is multiplication with
A smooth (semi)ring is a topological (semi)ring. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].