Theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mulMem'

Modification history

2024-05-29 09:23

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean

chore(RingTheory/GradedAlgebra/HomogeneousLocalization) New simp lemmas (#13037) …

Deleted AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mulMem'View on Github →

2023-07-07 04:14

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean

feat: port AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf (#5224)

Added AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mulMem'View on Github →