mem_idealSet — Mathlib

English

The fundamental cone intersects the ideal lattice to form the idealSet for a given integral ideal J.

Русский

Фундаментальный конус пересекается с идеальной решеткой, образуя idealSet для данного целого идеала J.

LaTeX

$$$\\text{idealSet}(K,J) = \\operatorname{fundamentalCone}(K) \\cap \\operatorname{idealLattice}(K, \\text{FractionalIdeal.mk0}(K,J)).$$$

Lean4

theorem mem_idealSet :
    x ∈ idealSet K J ↔
      x ∈ fundamentalCone K ∧ ∃ a : (𝓞 K), (a : 𝓞 K) ∈ (J : Set (𝓞 K)) ∧ mixedEmbedding K (a : 𝓞 K) = x :=
  by
  simp_rw [idealSet, Set.mem_inter_iff, idealLattice, SetLike.mem_coe, FractionalIdeal.coe_mk0, LinearMap.mem_range,
    LinearMap.coe_comp, LinearMap.coe_restrictScalars, coe_subtype, Function.comp_apply, AlgHom.toLinearMap_apply,
    RingHom.toIntAlgHom_coe, Subtype.exists, FractionalIdeal.mem_coe, FractionalIdeal.mem_coeIdeal, exists_prop',
    nonempty_prop, exists_exists_and_eq_and]

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