Commit 2023-03-29 09:00 87a0508b

View on Github →

feat: port RingTheory.Localization.Module (#3129)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Localization/Module.lean

added theorem Basis.localizationLocalization_apply

added theorem Basis.localizationLocalization_repr_algebraMap

added theorem LinearIndependent.iff_fractionRing

added theorem LinearIndependent.localization

added theorem LinearIndependent.localization_localization

added theorem SpanEqTop.localization_localization