theorem
L26 ↗of_ringEquiv
Module.Invertible.of_ringEquiv
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_Invertible_of_ringEquiv
universe u vLean source · statement
theorem _root_.Module.Invertible.of_ringEquiv
{R R' : Type u} [CommRing R] [CommRing R'] (σ : R ≃+* R')
(M : Type v) [AddCommGroup M] [Module R' M] [Module.Invertible R' M]
[Module R M] (hσ : ∀ (r : R) (m : M), r • m = σ r • m) :
Module.Invertible R M