IrreducibleRing

Statistics

Metric	Count
Definitions	0
Theorems `irreducible_of_irreducible_map_of_isPrime_nilradical`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`irreducible_of_irreducible_map_of_isPrime_nilradical` 📖	—	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Irreducible` `Polynomial` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.map`	—	—	`Ideal.instIsTwoSided_1` `nilradical_le_prime` `RingHom.instRingHomClass` `RingHom.ker_isPrime` `irreducible_of_irreducible_map` `Ideal.Quotient.isDomain` `map` `Polynomial.map_map` `Irreducible.not_isUnit` `RingHom.isUnit_map` `Polynomial.isUnit_iff` `Ideal.Quotient.noZeroDivisors` `Polynomial.coeff_map` `Polynomial.coeff_C` `Ideal.mk_ker` `Polynomial.isUnit_of_coeff_isUnit_isNilpotent` `isUnit_of_mul_isUnit_right` `instIsDedekindFiniteMonoid` `IsUnit.neg_iff` `add_sub_cancel_left` `sub_eq_add_neg` `sub_eq_iff_eq_add` `Finset.sum_range_succ` `Finset.Nat.sum_antidiagonal_eq_sum_range_succ` `Polynomial.coeff_mul` `IsNilpotent.isUnit_sub_one` `sum_mem` `Submodule.addSubmonoidClass` `Ideal.mul_mem_left` `mul_comm` `Irreducible.isUnit_or_isUnit` `Polynomial.map_mul`

---