toCharacterSpace_apply_eq_zero_of_mem

English

If a ∈ I, then the character I.toCharacterSpace evaluates to 0 at a.

Русский

Если a ∈ I, то характер I.toCharacterSpace принимает 0 на a.

LaTeX

$$$$I.toCharacterSpace(a) = 0$$$$

Lean4

theorem toCharacterSpace_apply_eq_zero_of_mem {a : A} (ha : a ∈ I) : I.toCharacterSpace a = 0 :=
  by
  unfold Ideal.toCharacterSpace
  simp only [CharacterSpace.equivAlgHom_symm_coe, AlgHom.coe_comp, AlgHom.coe_coe, Quotient.mkₐ_eq_mk,
    Function.comp_apply, NormedRing.algEquivComplexOfComplete_symm_apply]
  simp_rw [Quotient.eq_zero_iff_mem.mpr ha, spectrum.zero_eq]
  exact Set.eq_of_mem_singleton (Set.singleton_nonempty (0 : ℂ)).some_mem

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