NYLL
Module

Scheme_IdealSheafData_IsInvertible_pow.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_pow
1 declaration indexed from sourceView source ↗

Module documentation

Powers of invertible ideal sheaves

Invertibility is preserved by each natural-number power of ideal-sheaf data.

Imports1
Imported by67

Declarations

theorem

pow

L29 ↗
AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.pow
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_pow
universe u
open CategoryTheory AlgebraicGeometry
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.pow {X : Scheme.{u}} {I :
  X.IdealSheafData} (hI : I.IsInvertible) (n : ℕ) :
    (I ^ n).IsInvertible

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.