mul_eq_mul — Mathlib

English

If hf : IsMulFreimanHom 2 A B f and a,b,c,d ∈ A with a b = c d, then f a f b = f c f d.

Русский

Если hf : IsMulFreimanHom 2 A B f и a,b,c,d ∈ A с a b = c d, то f a f b = f c f d.

LaTeX

$$hf.mul_eq_mul ha hb hc hd h$$

Lean4

@[to_additive]
theorem mul_eq_mul (hf : IsMulFreimanHom 2 A B f) {a b c d : α} (ha : a ∈ A) (hb : b ∈ A) (hc : c ∈ A) (hd : d ∈ A)
    (h : a * b = c * d) : f a * f b = f c * f d :=
  by
  simp_rw [← prod_pair] at h ⊢
  refine hf.map_prod_eq_map_prod ?_ ?_ (card_pair _ _) (card_pair _ _) h <;> simp [ha, hb, hc, hd]

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