mul_eq_mul — Mathlib

English

For a FreimanIso hf between A and B, a,b,c,d ∈ A satisfy f a f b = f c f d iff a b = c d.

Русский

Для изоморфизма Фраймана hf между A и B выполняется f a f b = f c f d тогда и только если a b = c d.

LaTeX

$$hf.mul_eq_mul ha hb hc hd ↔ ab=cd$$

Lean4

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

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