Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-13 12:50 405ea5ce

View on Github →

feat(ring_theory/ring_hom/surjective): Meta properties about the surjectivity of ring homomorphisms (#17292) Also generalize several lemmas

Estimated changes

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

added theorem subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem

Modified src/algebra/module/projective.lean

Modified src/linear_algebra/finsupp.lean

added theorem finsupp.total_comp_lmap_domain

modified theorem finsupp.total_map_domain

Modified src/linear_algebra/linear_independent.lean

Created src/ring_theory/ring_hom/surjective.lean

added theorem ring_hom.surjective_of_localization_span

added theorem ring_hom.surjective_respects_iso

added theorem ring_hom.surjective_stable_under_base_change

added theorem ring_hom.surjective_stable_under_composition