# Commit 2020-07-08 14:31 f90fcc9e

View on Github →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:

```
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:

```
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 :=
```