Documentation Verification Report

AsSubring

📁 Source: Mathlib/RingTheory/Localization/AsSubring.lean

Statistics

Metric	Count
Definitions `mapToFractionRing`, `subalgebra`, `ofField`	3
Theorems `isFractionRing_range_mapToFractionRing`, `isLocalization_range_mapToFractionRing`, `mapToFractionRing_apply`, `map_isUnit_of_le`, `mem_range_mapToFractionRing_iff`, `instIsFractionRingSubtypeMemSubalgebra`, `isFractionRing`, `isFractionRing_ofField`, `isLocalization_ofField`, `isLocalization_subalgebra`, `mem_range_mapToFractionRing_iff_ofField`, `ofField_eq`	12
Total	15

Localization

Definitions

Name	Category	Theorems
`mapToFractionRing` 📖	CompOp	5 math math: `isFractionRing_range_mapToFractionRing`, `isLocalization_range_mapToFractionRing`, `subalgebra.mem_range_mapToFractionRing_iff_ofField`, `mapToFractionRing_apply`, `mem_range_mapToFractionRing_iff`
`subalgebra` 📖	CompOp	3 math math: `subalgebra.isLocalization_subalgebra`, `subalgebra.isFractionRing`, `subalgebra.ofField_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isFractionRing_range_mapToFractionRing` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`IsFractionRing` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `mapToFractionRing` `Subalgebra.toCommSemiring` `Subalgebra.toAlgebra` `Algebra.id`	—	`IsFractionRing.isFractionRing_of_isLocalization` `IsScalarTower.subalgebra'` `IsScalarTower.right` `isLocalization_range_mapToFractionRing`
`isLocalization_range_mapToFractionRing` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`IsLocalization` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `mapToFractionRing` `Subalgebra.toCommSemiring` `Subalgebra.algebra`	—	`IsLocalization.isLocalization_of_algEquiv` `map_isUnit_of_le` `IsLocalization.lift_injective_iff` `IsLocalization.injective` `IsFractionRing.injective` `Set.rangeFactorization_surjective`
`mapToFractionRing_apply` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`DFunLike.coe` `AlgHom` `AlgHom.funLike` `mapToFractionRing` `RingHom` `RingHom.instFunLike` `IsLocalization.lift` `algebraMap` `map_isUnit_of_le`	—	—
`map_isUnit_of_le` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`IsUnit` `MonoidWithZero.toMonoid` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap` `SetLike.instMembership` `Submonoid.instSetLike`	—	`IsLocalization.map_units`
`mem_range_mapToFractionRing_iff` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `mapToFractionRing` `IsLocalization.mk'` `Submonoid.instSetLike`	—	`IsLocalization.exists_mk'_eq` `IsLocalization.lift_mk'` `map_isUnit_of_le`

Localization.subalgebra

Definitions

Name	Category	Theorems
`ofField` 📖	CompOp	6 math math: `IsDedekindDomain.HeightOneSpectrum.iInf_localization_eq_bot`, `PrimeSpectrum.iInf_localization_eq_bot`, `isLocalization_ofField`, `isFractionRing_ofField`, `MaximalSpectrum.iInf_localization_eq_bot`, `ofField_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsFractionRingSubtypeMemSubalgebra` 📖	mathematical	—	`IsFractionRing` `Subalgebra` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SetLike.instMembership` `Subalgebra.instSetLike` `Subalgebra.toCommSemiring` `Semifield.toCommSemiring` `Subalgebra.toAlgebra` `CommSemiring.toSemiring` `Algebra.id`	—	`IsFractionRing.of_field` `Subalgebra.instFaithfulSMulSubtypeMem` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.self` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsFractionRing.div_surjective`
`isFractionRing` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`IsFractionRing` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `Localization.subalgebra` `Subalgebra.toCommSemiring` `Subalgebra.toAlgebra` `Algebra.id`	—	`IsFractionRing.isFractionRing_of_isLocalization` `IsScalarTower.subalgebra'` `IsScalarTower.right` `isLocalization_subalgebra`
`isFractionRing_ofField` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`IsFractionRing` `Subalgebra` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SetLike.instMembership` `Subalgebra.instSetLike` `ofField` `Subalgebra.toCommSemiring` `Semifield.toCommSemiring` `Subalgebra.toAlgebra` `Algebra.id`	—	`instIsFractionRingSubtypeMemSubalgebra`
`isLocalization_ofField` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`IsLocalization` `Subalgebra` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SetLike.instMembership` `Subalgebra.instSetLike` `ofField` `Subalgebra.toCommSemiring` `Semifield.toCommSemiring` `Subalgebra.algebra`	—	`ofField_eq` `isLocalization_subalgebra`
`isLocalization_subalgebra` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`IsLocalization` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `Localization.subalgebra` `Subalgebra.toCommSemiring` `Subalgebra.algebra`	—	`Subalgebra.copy_eq` `Localization.isLocalization_range_mapToFractionRing`
`mem_range_mapToFractionRing_iff_ofField` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`Subalgebra` `Field.toCommRing` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `Localization.mapToFractionRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `RingHom` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero`	—	`Localization.mem_range_mapToFractionRing_iff` `Submonoid.LocalizationMap.map_units` `Units.val_inv_eq_inv_val`
`ofField_eq` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`ofField` `Localization.subalgebra` `Field.toCommRing`	—	`Subalgebra.copy_eq`

---

← Back to Index