DualNumber

Mathlib.Algebra.DualNumber

URI: https://scilib.ai/kg/mathlib#DualNumber

← MathLib Explorer

English

If IsRelPrime x y, and x divides z and y divides z, then x·y divides z.

Русский

Если IsRelPrime(x,y), и x|z, и y|z, то x·y|z.

LaTeX

$$$\text{IsRelPrime}(x,y) \rightarrow (x \mid z) \rightarrow (y \mid z) \rightarrow (x \cdot y) \mid z$$$

Lean4

/-- The type of dual numbers, numbers of the form $a + bε$ where $ε^2 = 0$.
`R[ε]` is notation for `DualNumber R`. -/
abbrev DualNumber (R : Type*) : Type _ :=
  TrivSqZeroExt R R

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

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

Разделы

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

Аффилиация

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