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	Function.Exact AdicCompletion DFunLike.coe LinearMap Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup module LinearMap.instFunLike 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 DFunLike.coe LinearMap Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup module LinearMap.instFunLike 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 DFunLike.coe LinearMap Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup module LinearMap.instFunLike map	—	induction_on IsScalarTower.left SModEq.symm IsScalarTower.right ext

---

← Back to Index