18. Ring extensions
This page explains how to write a tower of ring extensions in Mathlib.
We assume that you have read Mathematics in Lean chapter 9 on Groups and Rings.
We will explain how Mathlib represents the following sentence:
"Let R, S and T be commutative rings, such that R is included in S and S is included in T."
Although we focus on commutative rings for simplicity, everything holds unless mentioned otherwise for semirings and fields.
See The non-unital, non-associative case for info on generalizing the assumptions further.