Commit 2022-07-30 19:08 348a674b

View on Github →

feat(algebra/algebra/subalgebra/basic): Swap arguments of map and comap (#15744) As suggested by @eric-wieser, I swapped the arguments of subalgebra.map and subalgebra.comap. I also updated subalgebra.map_injective to use function.injective and to have f implicit. This is done to make the subalgebra API match the subgroup, submodule, etc... API.

Estimated changes

Modified src/algebra/algebra/subalgebra/basic.lean

modified theorem algebra.comap_top

modified theorem algebra.map_bot

modified theorem algebra.map_top

modified def subalgebra.comap

modified theorem subalgebra.gc_map_comap

modified def subalgebra.map

modified theorem subalgebra.map_injective

Modified src/field_theory/intermediate_field.lean

modified def intermediate_field.map

Modified src/ring_theory/adjoin/fg.lean

Modified src/ring_theory/algebra_tower.lean