mem_traceDual_iff_isIntegral — Mathlib

English

For I ⊆ L as a Submodule over B, x ∈ Iᵛ iff ∀ a ∈ I, IsIntegral A (traceForm K L x a).

Русский

Для I ⊆ L по B: x ∈ Iᵛ тогда и только тогда, когда для всех a ∈ I выполняется, что traceForm(x,a) интегральна над A.

LaTeX

$$$x \in I^{\\vee} \iff \forall a \in I, \ IsIntegral A (traceForm K L (x) (a)).$$$

Lean4

theorem mem_traceDual_iff_isIntegral {I : Submodule B L} {x} : x ∈ Iᵛ ↔ ∀ a ∈ I, IsIntegral A (traceForm K L x a) :=
  forall₂_congr fun _ _ ↦ mem_one.trans IsIntegrallyClosed.isIntegral_iff.symm

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