div_C

Mathlib.Algebra.Polynomial.FieldDivision

URI: https://scilib.ai/kg/mathlib#Polynomial.div_C

English

As a corollary of dividing by C a, p / C a = p · C(a)⁻¹.

Русский

Следствие: p / C a = p · C(a)⁻¹.

LaTeX

$$p / C a = p * C a⁻¹$$

Lean4

theorem div_C : p / C a = p * C a⁻¹ := by simpa [mul_comm] using div_C_mul (q := 1)

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

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

Разделы

Аффилиация

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