Commit 2020-08-16 01:06 bf51f82a

feat(ring_theory/integral_closure): Rings lying within an integral extension are integral extensions (#3781) Proofs that if an algebra tower is integral then so are the two extensions making up the tower. I needed these for another proof I'm working on, but it seemed reasonable to create a smaller PR now since they are basically self contained.