isMulFreimanHom_const — Mathlib

English

A constant map f(x) = b with b ∈ B is a FreimanHom of any order n from A to B.

Русский

Постоянное отображение f(x) = b, где b ∈ B, является FreimanHom порядка n от A к B.

LaTeX

$$isMulFreimanHom_const {b} (hb : b ∈ B) : IsMulFreimanHom n A B (fun _ => b)$$

Lean4

@[to_additive]
theorem isMulFreimanHom_const {b : β} (hb : b ∈ B) : IsMulFreimanHom n A B fun _ ↦ b
    where
  mapsTo _ _ := hb
  map_prod_eq_map_prod s t _ _ hs ht _ := by simp only [map_const', hs, prod_replicate, ht]

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