Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-02 08:40 8a097f13

View on Github →

feat(ring_theory/ideal_operations): inj_iff_trivial_ker for ring homomorphisms (#951)

feat(ring_theory/ideal_operations): inj_iff_trivial_ker for ring homomorphisms
Update subgroup.lean
Update ideal_operations.lean

Estimated changes

Modified src/group_theory/subgroup.lean

added theorem is_group_hom.trivial_ker_iff_eq_one

Modified src/ring_theory/ideal_operations.lean

added theorem is_ring_hom.inj_iff_ker_eq_bot

added theorem is_ring_hom.injective_iff

added def is_ring_hom.ker

added theorem is_ring_hom.ker_eq

added theorem is_ring_hom.ker_eq_bot_iff_eq_zero