mathlib documentation

geometry.manifold.algebra.structures

@[instance]
def smooth_semiring.to_has_smooth_mul {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) (R : Type u_4) [semiring R] [topological_space R] [topological_semiring R] [charted_space H R] [s : smooth_semiring I R] :

@[class]
structure smooth_semiring {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) (R : Type u_4) [semiring R] [topological_space R] [topological_semiring R] [charted_space H R] :
Prop

A smooth semiring is a semiring where addition and multiplication are smooth.

Instances
@[instance]
def smooth_semiring.to_has_smooth_add {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) (R : Type u_4) [semiring R] [topological_space R] [topological_semiring R] [charted_space H R] [s : smooth_semiring I R] :

@[instance]
def smooth_ring.to_has_smooth_mul {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) (R : Type u_4) [ring R] [topological_space R] [topological_ring R] [charted_space H R] [s : smooth_ring I R] :

@[instance]
def smooth_ring.to_lie_add_group {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) (R : Type u_4) [ring R] [topological_space R] [topological_ring R] [charted_space H R] [s : smooth_ring I R] :

@[class]
structure smooth_ring {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) (R : Type u_4) [ring R] [topological_space R] [topological_ring R] [charted_space H R] :
Prop

A smooth ring is a ring where the ring operations are smooth.

Instances
@[instance]
def smooth_ring.to_smooth_semiring {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {H : Type u_2} [topological_space H] {E : Type u_3} [normed_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} {R : Type u_4} [ring R] [topological_space R] [topological_ring R] [charted_space H R] [t : smooth_ring I R] :

@[instance]
def field_smooth_ring {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] :
smooth_ring 𝓘(𝕜, 𝕜) 𝕜