liftOfLE_mk' — Mathlib

English

The image of mk' f1 m s under liftOfLE equals mk' f2 m ⟨s.1, h s.2⟩.

Русский

Образ mk' f1 m s под liftOfLE равен mk' f2 m ⟨s.1, h s.2⟩.

LaTeX

$$$$ \\text{liftOfLE}(\\text{mk' } f_1 m s) = \\text{mk' } f_2 m \\langle s.1, h s.2 \\rangle $$$$

Lean4

/-- The image of `m/s` under `liftOfLE` is `m/s`. -/
@[simp]
theorem liftOfLE_mk' (m : M) (s : S₁) : liftOfLE S₁ S₂ h f₁ f₂ (mk' f₁ m s) = mk' f₂ m ⟨s.1, h s.2⟩ :=
  by
  apply ((Module.End.isUnit_iff _).mp (map_units f₂ ⟨s, h s.2⟩)).1
  simp only [Module.algebraMap_end_apply, ← map_smul, ← Submonoid.smul_def, mk'_cancel']
  rw [liftOfLE, lift_apply]
  exact (mk'_cancel' (S := S₂) f₂ m ⟨s.1, h s.2⟩).symm

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