Commit 2020-08-03 17:57 b8df8aac

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.