Documentation Verification Report

Localization

📁 Source: Mathlib/LinearAlgebra/Dimension/Localization.lean

Statistics

Metric	Count
Definitions	0
Theorems `finrank_eq`, `finrank_eq_of_le_nonZeroDivisors`, `lift_rank_eq`, `lift_rank_eq_of_le_nonZeroDivisors`, `rank_eq`, `rank_eq_of_le_nonZeroDivisors`, `hasRankNullity`, `rank_eq`, `finrank_eq`, `lift_rank_eq`, `rank_eq`, `aleph0_le_rank_of_isEmpty_oreSet`, `exists_set_linearIndependent_of_isDomain`, `nonempty_oreSet_of_strongRankCondition`, `rank_quotient_add_rank_of_isDomain`	15
Total	15

IsBaseChange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finrank_eq` 📖	mathematical	`IsBaseChange` `AddCommGroup.toAddCommMonoid` `CommRing.toCommSemiring`	`Module.finrank` `CommSemiring.toSemiring`	—	`Cardinal.toNat_lift` `lift_rank_eq`
`finrank_eq_of_le_nonZeroDivisors` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero` `Algebra.algebraMapSubmonoid` `IsBaseChange` `AddCommGroup.toAddCommMonoid`	`Module.finrank`	—	`Cardinal.toNat_lift` `lift_rank_eq_of_le_nonZeroDivisors`
`lift_rank_eq` 📖	mathematical	`IsBaseChange` `AddCommGroup.toAddCommMonoid` `CommRing.toCommSemiring`	`Cardinal.lift` `Module.rank` `CommSemiring.toSemiring`	—	`FaithfulSMul.algebraMap_injective` `Function.Injective.noZeroDivisors` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `subsingleton_or_nontrivial` `RingHom.codomain_trivial` `rank_subsingleton` `Cardinal.lift_one` `isDomain_iff_noZeroDivisors_and_nontrivial` `Function.Injective.nontrivial` `IsFractionRing.injective` `Localization.isLocalization` `IsScalarTower.right` `TensorProduct.smulCommClass_left` `smulCommClass_self` `IsLocalization.tensorProduct_isLocalizedModule` `MulEquiv.isField` `Field.toIsField` `Algebra.TensorProduct.right_isScalarTower` `isLocalizedModule_iff_isLocalization` `Ne.isUnit` `IsDomain.toNontrivial` `map_ne_zero_of_mem_nonZeroDivisors` `OreLocalization.instSMulCommClass` `IsScalarTower.to_smulCommClass'` `Algebra.to_smulCommClass` `TensorProduct.isScalarTower_left` `RingHomCompTriple.ids` `LinearMap.IsScalarTower.compatibleSMul` `TensorProduct.isScalarTower` `OreLocalization.instIsScalarTower` `comp_iff` `isLocalizedModule_iff_isBaseChange` `Cardinal.lift_lift` `IsLocalizedModule.lift_rank_eq` `le_rfl` `IsLocalization.rank_eq` `lift_rank_eq_of_le_nonZeroDivisors` `IsScalarTower.left` `OreLocalization.instIsScalarTower_1` `localizedModuleIsLocalizedModule` `Module.Free.of_divisionRing` `IsNoetherianRing.strongRankCondition` `FractionRing.instNontrivial` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `map_le_nonZeroDivisors_of_injective` `Localization.instNoZeroDivisors` `EuclideanDomain.toNontrivial`
`lift_rank_eq_of_le_nonZeroDivisors` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero` `Algebra.algebraMapSubmonoid` `IsBaseChange` `AddCommGroup.toAddCommMonoid`	`Cardinal.lift` `Module.rank`	—	`Cardinal.lift_lift` `Algebra.to_smulCommClass` `IsLocalizedModule.lift_rank_eq` `IsLocalization.rank_eq` `Module.rank_baseChange` `Cardinal.lift_id'` `Cardinal.lift_umax` `TensorProduct.smulCommClass_left` `smulCommClass_self` `IsLocalization.tensorProduct_isLocalizedModule` `IsLocalization.tensorRight` `TensorProduct.isScalarTower_left` `IsScalarTower.right` `LinearEquiv.lift_rank_eq` `IsScalarTower.to_smulCommClass` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Algebra.TensorProduct.right_isScalarTower` `isLocalizedModule_iff_isBaseChange`
`rank_eq` 📖	mathematical	`IsBaseChange` `AddCommGroup.toAddCommMonoid` `CommRing.toCommSemiring`	`Module.rank` `CommSemiring.toSemiring`	—	`Cardinal.lift_id` `lift_rank_eq`
`rank_eq_of_le_nonZeroDivisors` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero` `Algebra.algebraMapSubmonoid` `IsBaseChange` `AddCommGroup.toAddCommMonoid`	`Module.rank`	—	`Cardinal.lift_id` `lift_rank_eq_of_le_nonZeroDivisors`

IsDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasRankNullity` 📖	mathematical	—	`HasRankNullity` `CommRing.toRing`	—	`exists_set_linearIndependent_of_isDomain` `rank_quotient_add_rank_of_isDomain`

IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rank_eq` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`Module.rank` `AddCommGroup.toAddCommMonoid`	—	`subsingleton_or_nontrivial` `RingHom.codomain_trivial` `rank_subsingleton` `injective` `le_antisymm` `Module.rank_def` `ciSup_le'` `faithfulSMul_iff_algebraMap_injective` `LinearIndependent.cardinal_le_rank` `LinearIndependent.restrict_scalars'` `IsScalarTower.right` `Function.Injective.nontrivial` `LinearIndependent.localization`

IsLocalizedModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finrank_eq` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`Module.finrank` `AddCommGroup.toAddCommMonoid`	—	`Cardinal.toNat_lift` `lift_rank_eq`
`lift_rank_eq` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`Cardinal.lift` `Module.rank` `AddCommGroup.toAddCommMonoid`	—	`subsingleton_or_nontrivial` `rank_subsingleton` `Cardinal.lift_one` `le_antisymm` `Module.rank_def` `Cardinal.lift_iSup` `Cardinal.bddAbove_range` `small_subtype` `small_set` `UnivLE.small` `UnivLE.self` `ciSup_le'` `LinearIndependent.cardinal_lift_le_rank` `linearIndependent_lift` `LinearIndependent.of_isLocalizedModule_of_isRegular` `le_nonZeroDivisors_iff_isRegular`
`rank_eq` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`Module.rank` `AddCommGroup.toAddCommMonoid`	—	`Cardinal.lift_id` `lift_rank_eq`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aleph0_le_rank_of_isEmpty_oreSet` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Cardinal.aleph0` `Module.rank` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Semiring.toModule`	—	`Mathlib.Tactic.Push.not_forall_eq` `OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `not_nonempty_iff` `Cardinal.aleph0_le` `LT.lt.not_ge` `zero_le` `Nat.instCanonicallyOrderedAdd` `Finset.sum_congr` `add_assoc` `zero_smul` `add_zero` `Finset.sum_range_succ'` `mul_right_cancel₀` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `Submonoid.instSubmonoidClass` `mem_nonZeroDivisors_iff_ne_zero` `IsDomain.toNontrivial` `Subtype.prop` `neg_mul` `neg_eq_iff_add_eq_zero` `pow_add` `pow_succ` `zero_add` `Fintype.linearIndependent_iff` `Fin.prop` `dite_mul` `Cardinal.mk_fintype` `Fintype.card_fin` `Cardinal.lift_natCast` `Cardinal.lift_uzero` `LinearIndependent.cardinal_lift_le_rank`
`exists_set_linearIndependent_of_isDomain` 📖	mathematical	—	`Set.Elem` `Module.rank` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearIndepOn`	—	`Module.Free.of_divisionRing` `IsDomain.toNontrivial` `IsDomain.to_noZeroDivisors` `IsLocalizedModule.linearIndependent_lift` `IsScalarTower.left` `IsScalarTower.right` `localizedModuleIsLocalizedModule` `LinearIndependent.restrict_scalars'` `OreLocalization.instIsScalarTower_1` `FractionRing.instFaithfulSMul` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.self` `Module.Basis.linearIndependent` `Cardinal.lift_injective` `Cardinal.mk_range_eq_of_injective` `LinearIndependent.injective` `Module.Free.rank_eq_card_chooseBasisIndex` `IsNoetherianRing.strongRankCondition` `FractionRing.instNontrivial` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `IsLocalization.rank_eq` `Localization.isLocalization` `le_rfl` `IsLocalizedModule.lift_rank_eq` `linearIndepOn_id_range_iff`
`nonempty_oreSet_of_strongRankCondition` 📖	mathematical	—	`OreLocalization.OreSet` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `nonZeroDivisors`	—	`aleph0_le_rank_of_isEmpty_oreSet` `LE.le.not_gt` `Module.rank_self` `Cardinal.one_lt_aleph0`
`rank_quotient_add_rank_of_isDomain` 📖	mathematical	—	`Cardinal` `Cardinal.instAdd` `Module.rank` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `CommRing.toRing` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	`Cardinal.lift_injective` `Cardinal.lift_add` `IsScalarTower.right` `IsScalarTower.left` `OreLocalization.instIsScalarTower_1` `IsLocalizedModule.lift_rank_eq` `Submodule.isLocalizedModule` `Localization.isLocalization` `localizedModuleIsLocalizedModule` `le_rfl` `instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient` `IsLocalization.rank_eq` `Submodule.Quotient.isScalarTower` `Submodule.isScalarTower'` `IsDomain.toNontrivial` `IsDomain.to_noZeroDivisors` `rank_quotient_add_rank_of_divisionRing`

---

← Back to Index