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	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike Module.Basis 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 DFunLike.coe LinearMap RingHom.id OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id LinearMap.instFunLike LocalizedModule.lift IsLocalizedModule.map_units Monoid.toMulOneClass Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder SetLike.le_def instIsConcreteLE Submonoid.powers_le 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