mathlib

f90fcc9e - chore(*): use is_algebra_tower instead of algebra.comap and generalize some constructions to semirings (#3299)

chore(*): use is_algebra_tower instead of algebra.comap and generalize some constructions to semirings (#3299) `algebra.comap` is now reserved to the **creation** of new algebra instances. For assumptions of theorems / constructions, `is_algebra_tower` is the new way to do it. For example: ```lean variables [algebra K L] [algebra L A] lemma is_algebraic_trans (L_alg : is_algebraic K L) (A_alg : is_algebraic L A) : is_algebraic K (comap K L A) := ``` is now written as: ```lean variables [algebra K L] [algebra L A] [algebra K A] [is_algebra_tower K L A] lemma is_algebraic_trans (L_alg : is_algebraic K L) (A_alg : is_algebraic L A) : is_algebraic K A := ```