multipliable_extend_one — Mathlib

English

Let g: β → γ be injective. Then Multipliable (extend g f 1) is equivalent to Multipliable f; extending the index set and filling new spots with 1 preserves multipliability.

Русский

Пусть g: β → γ — инъекция. Тогда Multipliable (extend g f 1) эквивалентно Multipliable f; расширение индексов и заполнение новых позиций единицей сохраняют мультиплиируемость.

LaTeX

$$$\text{Injective } g\;\Rightarrow\; \text{Multipliable } (\text{extend } g\, f\, 1) \iff \text{Multipliable } f$$$

Lean4

@[to_additive (attr := simp)]
theorem multipliable_extend_one {g : β → γ} (hg : Injective g) : Multipliable (extend g f 1) ↔ Multipliable f :=
  exists_congr fun _ ↦ hasProd_extend_one hg

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