Theorems · Inductive type · commutative algebra

Module.FaithfullyFlat

(R : Type u) → (M : Type v) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [Module R M] → Prop

A module M over a commutative ring R is faithfully flat if it is flat and, for all R-linear maps f : N → N' such that id ⊗ f = 0, we have f = 0.

Defined in

Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Cited by

72 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CommRingAddCommGroupModule