English
For modules F, K, A with tower F → K → A, the tower law holds: lift(rank_F K) · lift(rank_K A) = lift(rank_F A).
Русский
Для т tower F → K → A выполняется тождество рангов: lift(rank_F K) · lift(rank_K A) = lift(rank_F A).
LaTeX
$$$\\operatorname{lift}(\\operatorname{rank}_F K) \\cdot \\operatorname{lift}(\\operatorname{rank}_K A) = \\operatorname{lift}(\\operatorname{rank}_F A)$$$
Lean4
/-- Tower law: if `A` is a `K`-module and `K` is an extension of `F` then
$\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$.
The universe polymorphic version of `rank_mul_rank` below. -/
theorem lift_rank_mul_lift_rank :
Cardinal.lift.{w} (Module.rank F K) * Cardinal.lift.{v} (Module.rank K A) = Cardinal.lift.{v} (Module.rank F A) :=
by
let b := Module.Free.chooseBasis F K
let c := Module.Free.chooseBasis K A
rw [← (Module.rank F K).lift_id, ← b.mk_eq_rank, ← (Module.rank K A).lift_id, ← c.mk_eq_rank, ← lift_umax.{w, v}, ←
(b.smulTower c).mk_eq_rank, mk_prod, lift_mul, lift_lift, lift_lift, lift_lift, lift_lift, lift_umax.{v, w}]
