rename_surjective

Mathlib.Algebra.MvPolynomial.Rename

URI: https://scilib.ai/kg/mathlib#MvPolynomial.rename_surjective

← MathLib Explorer

English

If f is surjective, then rename f is surjective.

Русский

Если f сюръективна, то rename f сюръективна.

LaTeX

$$$\\text{rename}_f \\text{ is surjective if } f \\text{ is surjective}. $$$

Lean4

theorem rename_surjective (f : σ → τ) (hf : Function.Surjective f) :
    Function.Surjective (rename f : MvPolynomial σ R → MvPolynomial τ R) :=
  let ⟨_, hf⟩ := hf.hasRightInverse;
  rename_rightInverse hf |>.surjective

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru