Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_tensorPowSection_smul

theorem

tensorPowSection_smul

AlgebraicGeometry.Scheme.Modules.tensorPowSection_smul

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_tensorPowSection_smul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules in

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.tensorPowSection_smul {X :
  AlgebraicGeometry.Scheme.{u}} {L : X.Modules} {U : X.Opens} (g : Γ(X, U)) (s : Γ(L, U)) (n : ℕ) :
    AlgebraicGeometry.Scheme.Modules.tensorPowSection (g • s) n =
      g ^ n • AlgebraicGeometry.Scheme.Modules.tensorPowSection s n

Scheme_Modules_tensorPowSection_smul.lean

Module documentation

Scheme Modules tensor Pow Section smul

tensorPowSection_smul

Module documentation

Scheme Modules tensor Pow Section smul

Declarations

tensorPowSection_smul