Commit 2024-07-15 20:56 0d092ea7

View on Github →

feat(RingTheory/Unramified): Unramified + free => finite (#14478)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Kaehler/Basic.lean

added theorem KaehlerDifferential.ideal_fg

Created Mathlib/RingTheory/Unramified/Finite.lean

added theorem Algebra.FormallyUnramified.comp_sec

added def Algebra.FormallyUnramified.elem

added theorem Algebra.FormallyUnramified.finite_of_free

added theorem Algebra.FormallyUnramified.finite_of_free_aux

added theorem Algebra.FormallyUnramified.flat_of_restrictScalars

added theorem Algebra.FormallyUnramified.iff_exists_tensorProduct

added theorem Algebra.FormallyUnramified.lmul_elem

added theorem Algebra.FormallyUnramified.one_tmul_mul_elem

added theorem Algebra.FormallyUnramified.one_tmul_sub_tmul_one_mul_elem

added theorem Algebra.FormallyUnramified.projective_of_restrictScalars

added def Algebra.FormallyUnramified.sec

Modified docs/references.bib