of_bijective — Mathlib

English

Bijective ring homomorphisms are flat. In particular, any isomorphism of rings is flat.

Русский

Биективные гомоморфизмы колец являются плоскими. В частности, изоморфизмы колец плоские.

LaTeX

$$$$\text{If } f: R \to S \text{ is bijective, then } f \text{ is flat}.$$$$

Lean4

/-- Bijective ring maps are flat. -/
theorem of_bijective {f : R →+* S} (hf : Function.Bijective f) : Flat f :=
  by
  algebraize [f]
  exact Module.Flat.of_linearEquiv (LinearEquiv.ofBijective (Algebra.linearMap R S) hf).symm

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