mathlib documentation


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.

structure smooth_ring {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_add_comm_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) (R : Type u_4) [semiring R] [topological_space R] [charted_space H R] :

A smooth (semi)ring is a (semi)ring R where addition and multiplication are smooth. If R is a ring, then negation is automatically smooth, as it is multiplication with -1.

Instances of this typeclass
@[protected, instance]
@[protected, instance]
@[protected, instance]

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].