mk'_mul_mk'_of_map_mul — Mathlib

English

An equivalent formulation of mk'_eq_mk'_iff with alternative variables.

Русский

Эквивалентная формулировка mk'_eq_mk'_iff с альтернативными переменными.

LaTeX

$$$mk' f m_1 s_1 = mk' f m_2 s_2 \\iff \\exists s \\in S, s \\cdot s_1 \\cdot m_2 = s \\cdot s_2 \\cdot m_1$$$

Lean4

theorem mk'_mul_mk'_of_map_mul {M M' : Type*} [NonUnitalNonAssocSemiring M] [Semiring M'] [Module R M] [Algebra R M']
    (f : M →ₗ[R] M') (hf : ∀ m₁ m₂, f (m₁ * m₂) = f m₁ * f m₂) [IsLocalizedModule S f] (m₁ m₂ : M) (s₁ s₂ : S) :
    mk' f m₁ s₁ * mk' f m₂ s₂ = mk' f (m₁ * m₂) (s₁ * s₂) :=
  by
  symm
  apply (Module.End.algebraMap_isUnit_inv_apply_eq_iff _ _ _ _).mpr
  simp_rw [Submonoid.coe_mul, ← smul_eq_mul]
  rw [smul_smul_smul_comm, ← mk'_smul, ← mk'_smul]
  simp_rw [← Submonoid.smul_def, mk'_cancel, smul_eq_mul, hf]

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