Junyan Xu

Sorry, there seems to be a build error in Flat.lean

Personally I'm inclined to use the following as the definition: ``` /-- Two submodules K and L in an algebra S over R are linearly disjoint if the map `K...

> Yes, it requires flatness, at least for the items 1 and 2. Otherwise there is a counterexample: let R=Z, S=Z×Fp×Fp×Fp, let K be the submodule generated by (1,1,1,1) and...

Thanks 🎉 maintainer merge

New development at https://github.com/lean-forward/class-group-and-mordell-equation/blob/main/src/number_theory/quad_ring/basic.lean

Can you please fix the compile errors (which probably results from the implicitness changes)? Thanks!

Thanks 🎉 maintainer merge

Thanks! Since it's 1465 commits behind you probably want to merge master. maintainer delegate

I see, it's just [these two instances](https://github.com/leanprover-community/mathlib4/pull/18217/files#diff-39ff588cfd8afa83f18c2c9afa4e355f23c987dc7e99ab14a677f71ba9666ab7L818-L820) that can no longer be synthesized. maintainer merge