Subobjects

📁 Source: Mathlib/Algebra/Ring/Action/Subobjects.lean

Statistics

Metric	Count
Definitions mulSemiringAction, mulSemiringAction, instMulSemiringActionSubtypeMem	3
Theorems	0
Total	3

Subgroup

Definitions

Name	Category	Theorems
mulSemiringAction 📖	CompOp	24 math math: IsGaloisGroup.fixedPoints_top, IsGaloisGroup.quotientMap, IsGaloisGroup.fixedPoints_of_isGaloisGroup, IsGaloisGroup.of_fixedPoints_eq, IsDecompositionField.toIsGaloisGroup, IsGaloisGroup.fixedPoints_fixingSubgroup, IsGaloisGroup.le_fixedPoints_iff_le_fixingSubgroup, isInertiaField_iff, isDecompositionField_iff, Ideal.Quotient.stabilizerHomSurjectiveAuxFunctor_aux, IsGaloisGroup.fixingSubgroup_fixedPoints, IsGaloisGroup.fixedPoints_bot, instIsDecompositionFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupStabilizerIdealOfIsGalois, instIsInvariantSubtypeMemSubalgebraSubalgebraSubgroupQuotient, IsGaloisGroup.subgroup_iff, IsGaloisGroup.intermediateField, IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply, IsGaloisGroup.subgroup, IsInertiaField.toIsGaloisGroup, IsGaloisGroup.fixedPoints_le_of_le, instIsInertiaFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupInertiaOfIsGalois, IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup, instSMulCommClassQuotientSubgroupSubtypeMemSubalgebraSubalgebra, IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply_toDual

Submonoid

Definitions

Name	Category	Theorems
mulSemiringAction 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
instMulSemiringActionSubtypeMem 📖	CompOp	—

---

← Back to Index