Pi

📁 Source: Mathlib/RingTheory/Smooth/Pi.lean

Statistics

Metric	Count
Definitions	0
Theorems instForallOfFinite, of_pi, pi_iff	3
Total	3

Algebra.FormallySmooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instForallOfFinite 📖	mathematical	Algebra.FormallySmooth	Pi.commRing Pi.algebra CommRing.toCommSemiring Ring.toSemiring	—	pi_iff
of_pi 📖	mathematical	—	Algebra.FormallySmooth	—	of_split RingHom.instRingHomClass Ideal.instIsTwoSided_1 RingHomCompTriple.ids RingHom.map_one sub_eq_zero map_sub RingHomClass.toAddMonoidHomClass Ideal.Quotient.eq_zero_iff_mem AlgHomClass.toRingHomClass AlgHom.algHomClass Pi.single_eq_same sub_self IsScalarTower.left pow_two mul_sub sub_mul mul_one one_mul zero_sub neg_sub NegMemClass.neg_mem NonUnitalSubringClass.toNegMemClass instNonUnitalSubringClassIdeal Ideal.pow_mem_pow Pi.single_mul map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass AlgHom.ext
pi_iff 📖	mathematical	—	Algebra.FormallySmooth Pi.commRing Pi.algebra CommRing.toCommSemiring Ring.toSemiring	—	nonempty_fintype of_pi of_comp_surjective Ideal.instIsTwoSided_1 RingHom.instRingHomClass Ideal.pow_mem_pow Ideal.mk_ker CompleteOrthogonalIdempotents.lift_of_isNilpotent_ker CompleteOrthogonalIdempotents.map CompleteOrthogonalIdempotents.single Ideal.Quotient.mk_surjective CompleteOrthogonalIdempotents.bijective_pi Equiv.left_inv Equiv.right_inv MonoidHom.map_mul' RingHom.map_add' AlgHom.commutes' Ideal.Quotient.isScalarTower IsScalarTower.right Ideal.le_comap_map AlgHomClass.toRingHomClass AlgHom.algHomClass Ideal.instIsTwoSidedMapRingHomOfRingHomSurjective Ideal.Quotient.instRingHomSurjectiveQuotientMk Ideal.mem_span_singleton Set.image_singleton Ideal.map_span mul_assoc map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass mul_sub mul_one IsIdempotentElem.eq OrthogonalIdempotents.idem CompleteOrthogonalIdempotents.toOrthogonalIdempotents sub_self map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass MulZeroClass.zero_mul RingHomCompTriple.ids RingHom.map_one Ideal.Quotient.mk_eq_mk_iff_sub_mem dvd_refl map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass Pi.single_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass comp_surjective Ideal.map_pow Ideal.map_bot AlgHom.congr_fun AlgHom.ext AlgHom.toLinearMap_apply LinearMap.pi_ext' LinearMap.ext AlgEquiv.injective Pi.single_eq_same Ideal.Quotient.eq_zero_iff_mem sub_mul one_mul OrthogonalIdempotents.ortho sub_zero Pi.single_eq_of_ne MulZeroClass.mul_zero AlgEquiv.apply_symm_apply AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass sub_eq_zero mul_comm

---

← Back to Index