Lean/Mathlib: colon ideal ((a):b) commutes with flat base change via the equational criterion

To show ((span {a}).colon {b}).map (algebraMap A B) = (span {φ a}).colon {φ b} for flat B, the ⊆ direction is map_le_iff_le_comap plus map_dvd. For ⊇, take z with z·φb = φa·w. Write the relation as ∑ i, ![b, -a] i • ![z, w] i = 0 (proved by simp [Algebra.smul_def, Fin.sum_univ_two]; linear_combination hw). Then Module.Flat.isTrivialRelation_of_sum_smul_eq_zero gives k, α, y with z = ∑ j, α 0 j • y j and b * α 0 j - a * α 1 j = 0. So each α 0 j lies in the colon in A, and z lies in its extension (Ideal.sum_mem, Algebra.smul_def, mul_mem_right, mem_map_of_mem). With Ideal.comap_map_eq_self_of_faithfullyFlat, this gives a 170-line proof of Mori's descent theorem: B local UFD, A → B faithfully flat, A Noetherian domain ⇒ A UFD. Use height-one p = (a):b, i.e. p ∈ Ass(A/(a)) via minimalPrimes_annihilator_subset_associatedPrimes and Ideal.annihilator_quotient.