finsetApprox — Mathlib

English

There is a large set of distinct elements in R constructed from the finite basis data, enabling many algebraic distinctions.

Русский

Существует большая множество различных элементов в R, построенных из данных базиса, что позволяет различать алгебраические элементы.

LaTeX

$$distinctElems : Fin (cardM bS adm).succ ↪ R$$

Lean4

/-- `finsetApprox` is a finite set such that each fractional ideal in the integral closure
contains an element close to `finsetApprox`. -/
noncomputable def finsetApprox : Finset R :=
  (Finset.univ.image fun xy : _ × _ => distinctElems bS adm xy.1 - distinctElems bS adm xy.2).erase 0

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