iff_of_ringEquiv — Mathlib

English

Freeness of M over R is equivalent to freeness of M' over R' under RingEquiv data.

Русский

Свобода M над R эквивалентна свободе M' над R' при данных RingEquiv.

LaTeX

$$$$ \mathrm{Module.Free } R M \iff \mathrm{Module.Free } R' M' $$$$

Lean4

theorem iff_of_ringEquiv {R R' M M'} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R'] [AddCommMonoid M']
    [Module R' M'] (e₁ : R ≃+* R') (e₂ : M ≃ₛₗ[RingHomClass.toRingHom e₁] M') : Module.Free R M ↔ Module.Free R' M' :=
  ⟨fun _ ↦ of_ringEquiv e₁ e₂, fun _ ↦ of_ringEquiv e₁.symm e₂.symm⟩

Похожие утверждения