Theorems · Theorem · commutative algebra

IsLocalizedModule.iso_localizedModule_eq_refl

∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (M : Type u_2) [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M],
  IsLocalizedModule.iso S (LocalizedModule.mkLinearMap S M) = LinearEquiv.refl R (LocalizedModule S M)

The linear map (LocalizedModule S M) → (LocalizedModule S M) from iso is the identity.

Defined in

Mathlib.Algebra.Module.LocalizedModule.Basic

Cited by

2 results in Mathlib

Foundations

Depth 55 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidModule