Free

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

Statistics

Metric	Count
Definitions	0
Theorems exists_basis_localizedModule_powers, exists_free_localizedModule_powers	2
Total	2

Module.FinitePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_basis_localizedModule_powers 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring LocalizedModule Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommGroup.toAddCommMonoid OreLocalization.instAddCommMonoidOreLocalization OreLocalization.oreSetComm CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id LinearMap.instFunLike LocalizedModule.lift IsLocalizedModule.map_units Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Monoid.toMulOneClass Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder SetLike.le_def instIsConcreteLE Submonoid.powers_le Module.Basis Localization CommRing.toCommMonoid CommMonoid.toMonoid OreLocalization.instSemiring Ring.toSemiring CommRing.toRing OreLocalization.instModule Module.Basis.instFunLike	—	Module.finitePresentation_of_projective Module.Projective.of_free Module.Free.finsupp Module.Free.self Module.Finite.finsupp Module.Finite.self RingHomInvPair.ids IsScalarTower.left IsScalarTower.right RingHomCompTriple.ids IsLocalizedModule.map_units instIsLocalizedModuleFinsuppLinearMap instIsLocalizedModuleLinearMapOfIsLocalization SetLike.le_def instIsConcreteLE Submonoid.powers_le LinearMap.IsScalarTower.compatibleSMul OreLocalization.instIsScalarTower_1 LinearMap.CompatibleSMul.finsupp_cod exists_lift_equiv_of_isLocalizedModule Localization.isLocalization Finsupp.isScalarTower LinearEquiv.left_inv LinearEquiv.right_inv LinearMap.congr_fun IsLocalizedModule.iso_symm_comp LinearEquiv.injective LinearEquiv.apply_symm_apply Module.Basis.repr_self LinearMap.map_zero Finsupp.mapRange_single map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass smulCommClass_self IsUnit.unit.congr_simp IsUnit.unit_one inv_one
exists_free_localizedModule_powers 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike Module.Free Localization CommRing.toCommMonoid Submonoid.powers CommMonoid.toMonoid LocalizedModule MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommGroup.toAddCommMonoid OreLocalization.instSemiring Ring.toSemiring CommRing.toRing OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization CommSemiring.toCommMonoid Module.toDistribMulAction OreLocalization.instModule Module.finrank	—	Module.Finite.of_isLocalizedModule instFiniteOfFinitePresentation IsScalarTower.left IsScalarTower.right IsLocalizedModule.map_units SetLike.le_def instIsConcreteLE Submonoid.powers_le exists_basis_localizedModule_powers Finite.of_fintype RingHom.domain_nontrivial Localization.isLocalization MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Module.Free.of_basis Module.finrank_eq_nat_card_basis commRing_strongRankCondition

---

← Back to Index