IsResidueAlgebra

📁 Source: FLT/Deformations/IsResidueAlgebra.lean

Statistics

Metric	Count
Definitions IsResidueAlgebra, algEquiv, preimage	3
Theorems algebraMap_bijective, algebraMap_surjective, exists_sub_mem_maximalIdeal, inst, instQuotientIdeal, isSurjective', of_restrictScalars, preimage_spec, residue_preimage, residue_preimage_eq_iff	10
Total	13

IsResidueAlgebra

Definitions

Name	Category	Theorems
algEquiv 📖	CompOp	—
preimage 📖	CompOp	4 math math: residue_preimage_eq_iff, preimage_spec, Deformation.ProartinianCat.to_residueField_apply, residue_preimage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_bijective 📖	—	—	—	—	algebraMap_surjective
algebraMap_surjective 📖	—	—	—	—	isSurjective'
exists_sub_mem_maximalIdeal 📖	—	—	—	—	algebraMap_surjective
inst 📖	mathematical	—	IsResidueAlgebra	—	—
instQuotientIdeal 📖	mathematical	—	IsResidueAlgebra IsLocalRing.quot	—	IsLocalRing.quot IsLocalRing.ResidueField.map_surjective algebraMap_surjective
isSurjective' 📖	—	—	—	—	—
of_restrictScalars 📖	mathematical	—	IsResidueAlgebra	—	algebraMap_surjective
preimage_spec 📖	mathematical	—	preimage	—	exists_sub_mem_maximalIdeal
residue_preimage 📖	mathematical	—	preimage	—	preimage_spec
residue_preimage_eq_iff 📖	mathematical	—	preimage	—	algebraMap_bijective residue_preimage

(root)

Definitions

Name	Category	Theorems
IsResidueAlgebra 📖	CompData	4 math math: IsResidueAlgebra.inst, IsResidueAlgebra.of_restrictScalars, Deformation.IsLocalProartinianAlgebra.toIsResidueAlgebra, IsResidueAlgebra.instQuotientIdeal

---

← Back to Index