ofCharZero

Mathlib.Algebra.CharP.Defs

URI: https://scilib.ai/kg/mathlib#CharP.ofCharZero

English

If two CharP predicates hold on R with possibly different p,q, then p = q.

Русский

Если на R выполняются CharP с разными p,q, то p = q.

LaTeX

$$$\text{CharP}(R,p) \land \text{CharP}(R,q) \Rightarrow p = q.$$$

Lean4

instance ofCharZero [CharZero R] : CharP R 0 where
  cast_eq_zero_iff x := by rw [zero_dvd_iff, ← Nat.cast_zero, Nat.cast_inj]

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

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

Разделы

Аффилиация

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