mul — Mathlib

English

Equivalent Freiman-isomorphism when both domain and codomain are empty: any f gives an isomorphism.

Русский

Эквивалентность Фримановой изоморфии при пустых множествах: любой f задаёт изоморфию.

LaTeX

$$$IsMulFreimanIso n (\\emptyset : Set α) (\\emptyset : Set β) f$$$

Lean4

@[to_additive]
theorem mul (h₁ : IsMulFreimanHom n A B₁ f₁) (h₂ : IsMulFreimanHom n A B₂ f₂) : IsMulFreimanHom n A (B₁ * B₂) (f₁ * f₂)
    where
  mapsTo := h₁.mapsTo.mul h₂.mapsTo
  map_prod_eq_map_prod s t hsA htA hs ht
    h := by
    rw [Pi.mul_def, prod_map_mul, prod_map_mul, h₁.map_prod_eq_map_prod hsA htA hs ht h,
      h₂.map_prod_eq_map_prod hsA htA hs ht h]

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