integerSetEquivNorm_apply_fst — Mathlib

English

The fst projection of the norm equivalence agrees with the ideal preimage construction.

Русский

Проекция fst в эквивалентности норм согласуется с построением предобраза идеала.

LaTeX

$$$((\\operatorname{integerSetEquivNorm}(K,n))_{\\text{fst}}\\;a).val = \\operatorname{Ideal.span}(...)$$$

Lean4

@[simp]
theorem integerSetEquivNorm_apply_fst {n : ℕ} (a : { a : integerSet K // mixedEmbedding.norm (a : mixedSpace K) = n }) :
    ((integerSetEquivNorm K n a).1 : Ideal (𝓞 K)) = span {(preimageOfMemIntegerSet a.val : 𝓞 K)} := by
  simp_rw [integerSetEquivNorm, Equiv.prodSubtypeFstEquivSubtypeProd, Equiv.trans_def, Equiv.prodCongrLeft,
    Equiv.trans_apply, Equiv.subtypeEquiv_apply, Equiv.coe_fn_mk, Equiv.subtypeSubtypeEquivSubtypeInter_apply_coe,
    integerSetEquiv_apply_fst]

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