eq_and — Mathlib

English

FaithfullyFlat is equal to the predicate mapping f to Flat(f) and Surjective(f.specComap).

Русский

FaithfullyFlat эквивалентно отображению f → (Flat(f) ∧ Surjective(f.specComap)).

LaTeX

$$$\\operatorname{FaithfullyFlat} =\\; f \\mapsto (f.Flat \\wedge \\operatorname{Surjective}(f.specComap))$$$

Lean4

theorem eq_and : FaithfullyFlat = fun (f : R →+* S) ↦ f.Flat ∧ Function.Surjective f.specComap :=
  by
  ext
  rw [iff_flat_and_comap_surjective]

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