Module.Flat.ker_of_surjective_of_flat
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_ker_of_surjective_of_flat
universe u
open TensorProductLean source · statement
theorem _root_.Module.Flat.ker_of_surjective_of_flat
{R : Type u} [CommRing R] {M P : Type u}
[AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P]
[Module.Flat R M] [Module.Flat R P] (g : M →ₗ[R] P) (hg : Function.Surjective g) :
Module.Flat R (LinearMap.ker g)