Documentation Verification Report

GeometricallyReduced

📁 Source: Mathlib/RingTheory/Nilpotent/GeometricallyReduced.lean

Statistics

Metric	Count
Definitions `IsGeometricallyReduced`, `GeometricallyReduced`	2
Theorems `isReduced_algebraicClosure_tensorProduct`, `of_forall_fg`, `of_injective`, `instIsReducedTensorProductOfIsAlgebraicOfIsGeometricallyReduced`, `isGeometricallyReduced_iff`, `isReduced_of_isGeometricallyReduced`	6
Total	8

Algebra

Definitions

Name	Category	Theorems
`IsGeometricallyReduced` 📖	CompData	2 math math: `isGeometricallyReduced_iff`, `IsGeometricallyReduced.of_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsReducedTensorProductOfIsAlgebraicOfIsGeometricallyReduced` 📖	mathematical	—	`IsReduced` `TensorProduct` `Semifield.toCommSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Ring.toSemiring` `TensorProduct.zero` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `TensorProduct.instSemiring`	—	`isReduced_of_injective` `IsScalarTower.to_smulCommClass` `IsScalarTower.left` `AlgebraicClosure.instIsScalarTower` `IsScalarTower.right` `RingHomClass.toMonoidWithZeroHomClass` `to_smulCommClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgebraicClosure.isAlgClosed` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Module.Flat.rTensor_preserves_injective_linearMap` `Module.Flat.of_free` `Module.Free.of_divisionRing` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsGeometricallyReduced.isReduced_algebraicClosure_tensorProduct`
`isGeometricallyReduced_iff` 📖	mathematical	—	`IsGeometricallyReduced` `IsReduced` `TensorProduct` `Semifield.toCommSemiring` `Field.toSemifield` `AlgebraicClosure` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AlgebraicClosure.instCommRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgebraicClosure.instField` `AlgebraicClosure.instAlgebra` `id` `Ring.toSemiring` `TensorProduct.zero` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `TensorProduct.instSemiring`	—	—
`isReduced_of_isGeometricallyReduced` 📖	mathematical	—	`IsReduced` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	—	`isReduced_of_injective` `RingHomClass.toMonoidWithZeroHomClass` `to_smulCommClass` `IsScalarTower.right` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `TensorProduct.includeRight_injective` `Module.Flat.of_free` `Module.Free.of_divisionRing` `FaithfulSMul.algebraMap_injective` `Module.Free.instFaithfulSMulOfNontrivial` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsGeometricallyReduced.isReduced_algebraicClosure_tensorProduct`

Algebra.IsGeometricallyReduced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isReduced_algebraicClosure_tensorProduct` 📖	mathematical	—	`IsReduced` `TensorProduct` `Semifield.toCommSemiring` `Field.toSemifield` `AlgebraicClosure` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AlgebraicClosure.instCommRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgebraicClosure.instField` `AlgebraicClosure.instAlgebra` `Algebra.id` `Ring.toSemiring` `TensorProduct.zero` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Algebra.TensorProduct.instSemiring`	—	—
`of_forall_fg` 📖	—	`Algebra.IsGeometricallyReduced` `Subalgebra` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Subalgebra.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Subalgebra.algebra`	—	—	`IsReduced.tensorProduct_of_flat_of_forall_fg` `Module.Flat.of_free` `Module.Free.of_divisionRing`
`of_injective` 📖	mathematical	`DFunLike.coe` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring` `AlgHom.funLike`	`Algebra.IsGeometricallyReduced`	—	`isReduced_of_injective` `IsScalarTower.to_smulCommClass` `AlgebraicClosure.instIsScalarTower` `IsScalarTower.right` `RingHomClass.toMonoidWithZeroHomClass` `Algebra.to_smulCommClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Module.Flat.lTensor_preserves_injective_linearMap` `Module.Flat.of_free` `Module.Free.of_divisionRing` `isReduced_algebraicClosure_tensorProduct`

AlgebraicGeometry

Definitions

Name	Category	Theorems
`GeometricallyReduced` 📖	CompData	9 math math: `instGeometricallyReducedSndScheme`, `instGeometricallyReducedFiberToSpecResidueField`, `geometricallyReduced_iff`, `instGeometricallyReducedFstScheme`, `instGeometricallyReducedMorphismRestrict`, `GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible`, `instIsStableUnderBaseChangeSchemeGeometricallyReduced`, `GeometricallyReduced.eq_geometrically`, `instGeometricallyReducedOfGeometricallyIntegral`

---

← Back to Index