mathlib

b8df8aac - feat(algebra/ring): the codomain of a ring hom is trivial iff ... (#3676)

feat(algebra/ring): the codomain of a ring hom is trivial iff ... (#3676) In the discussion of #3488, Johan (currently on vacation, so I'm not pinging him) noted that we were missing the lemma "if `f` is a ring homomorphism, `∀ x, f x = 0` implies that the codomain is trivial". This PR adds a couple of ways to derive from homomorphisms that rings are trivial. I used `0 = 1` to express that the ring is trivial because that seems to be the one that is used in practice. Co-authored-by: Vierkantor <vierkantor@vierkantor.com>