English
Tower law in a simpler setting: rank_F K · rank_K A = rank_F A.
Русский
Упрощённое тождество: rank_F K · rank_K A = rank_F A.
LaTeX
$$$\\operatorname{rank}_F K \\cdot \\operatorname{rank}_K A = \\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)$.
This is a simpler version of `lift_rank_mul_lift_rank` with `K` and `A` in the same universe. -/
@[stacks 09G9]
theorem rank_mul_rank (A : Type v) [AddCommMonoid A] [Module K A] [Module F A] [IsScalarTower F K A] [Module.Free K A] :
Module.rank F K * Module.rank K A = Module.rank F A := by convert lift_rank_mul_lift_rank F K A <;> rw [lift_id]
