Exactness

📁 Source: Mathlib/RingTheory/AdicCompletion/Exactness.lean

Statistics

Metric	Count
Definitions	0
Theorems map_exact, map_injective, map_surjective	3
Total	3

AdicCompletion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_exact 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike Function.Exact NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule instCommRing instAddCommGroup module map instZero	—	LinearMap.exact_of_comp_eq_zero_of_ker_le_range RingHomCompTriple.ids map_comp Function.Exact.linearMap_comp_eq_zero map_zero induction_on RingHomSurjective.ids IsScalarTower.left IsScalarTower.right Ideal.exists_pow_inf_eq_pow_smul SModEq.symm AddLeftCancelSemigroup.toIsLeftCancelAdd ext Submodule.Quotient.eq Submodule.smul_mono_left Ideal.pow_le_pow_right
map_injective 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule instCommRing instAddCommGroup module map	—	IsScalarTower.left IsScalarTower.right RingHomSurjective.ids Ideal.exists_pow_inf_eq_pow_smul LinearMap.ker_eq_bot LinearMap.ker_eq_bot' induction_on mk_zero_of Submodule.comap_map_eq_of_injective Submodule.map_smul'' Submodule.map_top smul_mono_right Submodule.instCovariantClassHSMulLe_1 inf_le_right
map_surjective 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule instCommRing instAddCommGroup module map	—	induction_on IsScalarTower.left SModEq.symm IsScalarTower.right ext

---

← Back to Index