finite_iff_isIntegral_and_finiteType

English

For a ring hom f, finiteness is equivalent to being integral and of finite type.

Русский

Для гомоморфизма f равносильно быть интегральным и иметь конечный тип.

LaTeX

$$$f.Finite \\iff (f.IsIntegral) \\land (f.FiniteType)$$$

Lean4

/-- finite = integral + finite type -/
theorem finite_iff_isIntegral_and_finiteType : f.Finite ↔ f.IsIntegral ∧ f.FiniteType :=
  ⟨fun h ↦ ⟨h.to_isIntegral, h.to_finiteType⟩, fun ⟨h, h'⟩ ↦ h.to_finite h'⟩

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