Tuples of algebraic integers

Basic facts about tuples y : ι → 𝓞 K of algebraic integers and their images in K.

Main results

• NumberField.RingOfIntegers.coe_tuple_eq_zero_iff: a tuple of algebraic integers is zero exactly when its image in K is zero.

@[simp]

theorem NumberField.RingOfIntegers.coe_tuple_eq_zero_iff {K : Type u_1} [Field K] {ι : Type u_2} {y : ι → RingOfIntegers K} : (fun (i : ι) => ↑(y i)) = 0 ↔ y = 0

A tuple of algebraic integers is zero exactly when its image in K is zero.