ProjSpaceCech_Twist_d_sq.lean

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_d_sq
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section AltCech
variable (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_d_sq
universe u
noncomputable section
open Finset Function
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs in