of_equiv — Mathlib

English

If e: Q ≃_ℓ[R] M is a linear equivalence and Q is a Baer R-module, then M is Baer as well.

Русский

Если имеется линейное эквивалиентное отображение e: Q ≃_ℓ[R] M и Q — модуль Баера, то и M является Baer-модулем.

LaTeX

$$$ \text{of\_equiv}(e,f) : \text{Module.Baer } R Q \rightarrow \text{Module.Baer } R M$$$

Lean4

theorem of_equiv (e : Q ≃ₗ[R] M) (h : Module.Baer R Q) : Module.Baer R M := fun I g ↦
  have ⟨g', h'⟩ := h I (e.symm ∘ₗ g)
  ⟨e ∘ₗ g', by simpa [LinearEquiv.eq_symm_apply] using h'⟩

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