Theorems · Theorem · commutative algebra

Module.Invertible.bijective

∀ {R : Type u} {M : Type v} {inst : CommSemiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M}
  [self : Module.Invertible R M], Function.Bijective ⇑(contractLeft R M)

Defined in

Mathlib.RingTheory.PicardGroup

Cited by

1 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Quot.sound

Assumes

Module.Invertible