mathlib3 documentation


Smooth structures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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