pi — Mathlib · SciLib

English

A definition asserting that N1 ≤ N2 and the quotient N2/N1 is isomorphic to A/p for some prime p.

Русский

Определение: N1 ≤ N2 и (N2/N1) ≅ A/p для некоторого простого p.

LaTeX

$$$\\text{IsQuotientEquivQuotientPrime}(N_1,N_2) := N_1 \\le N_2 \\land \\exists p \\; (p\\ \\text{prime}) \\land (N_2/N_1) \\cong A/p.$$$

Lean4

/-- `Πᵢ Iᵢ` as an ideal of `Πᵢ Rᵢ`. -/
def pi : Ideal (Π i, R i) where
  carrier := {r | ∀ i, r i ∈ I i}
  zero_mem' i := (I i).zero_mem
  add_mem' ha hb i := (I i).add_mem (ha i) (hb i)
  smul_mem' a _b hb i := (I i).mul_mem_left (a i) (hb i)

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