Commit 2023-07-08 03:58 be1b0695

View on Github →

feat: port AlgebraicGeometry.ProjectiveSpectrum.Scheme (#5767)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.add_mem

added def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asHomogeneousIdeal

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal.homogeneous

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal.ne_top

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal.prime

added def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.denom_not_mem

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.relevant

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.smul_mem

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.zero_mem

added def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff'

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff

added def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.toFun

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.MemCarrier.clear_denominator'

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.MemCarrier.clear_denominator

added def AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier_ne_top

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.disjoint

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mem_carrier_iff

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_eq

added def AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun

added def AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec