Mathlib v3 is deprecated. Go to Mathlib v4

Theorem pi.ring_hom_injective

Modification history

2021-08-10 09:12
src/algebra/ring/pi.lean
feat(algebra/group/pi): Add `pi.const_(monoid|add_monoid|ring|alg)_hom` (#8518)
Added pi.ring_hom_injectiveView on Github →