count_coe_nonneg

Mathlib.RingTheory.DedekindDomain.Factorization

URI: https://scilib.ai/kg/mathlib#FractionalIdeal.count_coe_nonneg

← MathLib Explorer

English

For any ideal J, 0 ≤ count(K, v, coeIdeal(J)).

Русский

Для любого идеала J верно 0 ≤ count(K, v, coeIdeal(J)).

LaTeX

$$$$ 0 \\leq \\operatorname{count}(K,v, \\mathrm{coeIdeal}(J)). $$$$

Lean4

theorem count_coe_nonneg (J : Ideal R) : 0 ≤ count K v J :=
  by
  by_cases hJ : J = 0
  · simp only [hJ, Submodule.zero_eq_bot, coeIdeal_bot, count_zero, le_refl]
  · classical simp only [count_coe K v hJ, Nat.cast_nonneg]

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

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

Разделы

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

Аффилиация

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