Commit 2023-04-30 11:38 42f68caa

View on Github →

feat: port FieldTheory.Tower (#3716)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/Tower.lean

added theorem FiniteDimensional.Subalgebra.isSimpleOrder_of_finrank_prime

added theorem FiniteDimensional.finrank_linear_map'

added theorem FiniteDimensional.finrank_mul_finrank'

added theorem FiniteDimensional.finrank_mul_finrank

added theorem FiniteDimensional.left

added theorem FiniteDimensional.right

added theorem FiniteDimensional.trans

added theorem lift_rank_mul_lift_rank

added theorem rank_mul_rank