comp — Mathlib

English

The composition of FreimanHom n B C g and FreimanHom n A B f is a FreimanHom n A C (g ∘ f).

Русский

Вычисление композиции FreimanHom: g ∘ f образует FreimanHom n A C.

LaTeX

$$IsMulFreimanHom n A C (g ∘ f)$$

Lean4

@[to_additive]
theorem comp (hg : IsMulFreimanHom n B C g) (hf : IsMulFreimanHom n A B f) : IsMulFreimanHom n A C (g ∘ f)
    where
  mapsTo := hg.mapsTo.comp hf.mapsTo
  map_prod_eq_map_prod s t hsA htA hs ht
    h := by
    rw [← map_map, ← map_map]
    refine
      hg.map_prod_eq_map_prod ?_ ?_ (by rwa [card_map]) (by rwa [card_map]) (hf.map_prod_eq_map_prod hsA htA hs ht h)
    · simpa using fun a h ↦ hf.mapsTo (hsA h)
    · simpa using fun a h ↦ hf.mapsTo (htA h)

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