Commit 2022-04-09 22:07 e3a8ef1c

View on Github →

feat(algebra/algebra/*): generalise (#13252) Some generalisations straight from Alex's generalisation linter, with some care about how to place them. Some algebra lemmas are weakened to semirings, allowing us to talk about ℕ-algebras much more easily.

Estimated changes

Modified src/algebra/algebra/basic.lean

modified theorem algebra.mem_algebra_map_submonoid_of_mem

modified theorem ring_hom.map_rat_algebra_map

Modified src/algebra/algebra/operations.lean

modified theorem submodule.mem_span_mul_finite_of_mem_span_mul

Modified src/algebra/algebra/spectrum.lean

deleted theorem is_unit.smul_sub_iff_sub_inv_smul

modified theorem spectrum.exists_mem_of_not_is_unit_aeval_prod

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

Modified src/algebra/algebra/tower.lean

Modified src/algebra/algebra/unitization.lean

modified theorem unitization.coe_add

modified theorem unitization.coe_mul

modified theorem unitization.coe_mul_inl

modified theorem unitization.inl_mul_coe

Modified src/group_theory/group_action/group.lean

added theorem is_unit.smul_sub_iff_sub_inv_smul

modified theorem is_unit_smul_iff