instFreeCotangentSpaceToExtension

English

The cotangent space P.toExtension.CotangentSpace is a free module over S with basis P.cotangentSpaceBasis.

Русский

Котантгенциальное пространство P.toExtension.CotangentSpace является свободным модулем над S базисом P.cotangentSpaceBasis.

LaTeX

$$Module.Free S P.toExtension.CotangentSpace$$

Lean4

instance (P : Generators R S ι) : Module.Free S P.toExtension.CotangentSpace :=
  .of_basis P.cotangentSpaceBasis

Похожие утверждения