Pi

Statistics

Name	Kind	Assumes	Proves	Validates	Depends On
`instForall` 📖	mathematical	`Algebra.FormallyUnramified`	`Pi.commRing` `Pi.algebra` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`pi_iff`
`pi_iff` 📖	mathematical	—	`Algebra.FormallyUnramified` `Pi.commRing` `Pi.algebra` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`nonempty_fintype` `of_surjective` `Function.surjective_eval` `Zero.instNonempty` `Ideal.instIsTwoSided_1` `iff_comp_injective` `AlgHom.ext` `Finset.univ_sum_single` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Finset.sum_congr` `Ideal.Quotient.eq_zero_iff_mem` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `sub_eq_zero` `AlgHom.congr_fun` `mul_one` `Ideal.mem_bot` `IsIdempotentElem.eq` `IsIdempotentElem.mul` `IsIdempotentElem.map` `NonUnitalAlgSemiHomClass.toMulHomClass` `IsIdempotentElem.one_sub` `pow_two` `Ideal.pow_mem_pow` `mul_sub` `Ideal.mul_mem_left` `neg_mul` `neg_sub` `mul_comm` `RingHomCompTriple.ids` `RingHom.map_one` `Ideal.mem_span_singleton` `dvd_refl` `Pi.single_mul` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `comp_injective` `IsScalarTower.right` `Ideal.map_pow` `Ideal.map_bot` `Ideal.mem_map_of_mem` `one_mul` `MulZeroClass.zero_mul` `sub_self` `mul_assoc`

---