Operations

📁 Source: Mathlib/Algebra/Algebra/Subalgebra/Operations.lean

Statistics

Metric	Count
Definitions subalgebra, subring, subsemiring	3
Theorems ker_rangeRestrict, mem_of_finset_sum_eq_one_of_pow_smul_mem, mem_of_span_eq_top_of_smul_pow_mem	3
Total	6

AlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ker_rangeRestrict 📖	mathematical	—	RingHom.ker Subalgebra SetLike.instMembership Subalgebra.instSetLike range AlgHom Subalgebra.toSemiring Subalgebra.algebra funLike AlgHomClass.toRingHomClass algHomClass rangeRestrict	—	Ideal.ext AlgHomClass.toRingHomClass algHomClass

FixedPoints

Definitions

Name	Category	Theorems
subalgebra 📖	CompOp	3 math math: Ideal.Quotient.stabilizerHomSurjectiveAuxFunctor_aux, instIsInvariantSubtypeMemSubalgebraSubalgebraSubgroupQuotient, instSMulCommClassQuotientSubgroupSubtypeMemSubalgebraSubalgebra
subring 📖	CompOp	—
subsemiring 📖	CompOp	2 math math: IsGaloisGroup.algebraMap_ringEquivFixedPoints_symm_apply, IsGaloisGroup.ringEquivFixedPoints_apply_coe

Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_of_finset_sum_eq_one_of_pow_smul_mem 📖	mathematical	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Subalgebra SetLike.instMembership instSetLike Algebra.toSMul Algebra.id Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	Subalgebra CommSemiring.toSemiring SetLike.instMembership instSetLike	—	AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass instSubsemiringClass map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Finset.sum_congr map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Ideal.eq_top_iff_one sum_mem Submodule.addSubmonoidClass Ideal.mul_mem_left Ideal.subset_span Set.mem_image_of_mem Ideal.span_pow_eq_top Submodule.mem_of_span_top_of_smul_mem SubsemiringClass.toSubmonoidClass tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub Finset.le_sup pow_add SubmonoidClass.toMulMemClass SemigroupAction.mul_smul Submodule.smul_mem pow_mem
mem_of_span_eq_top_of_smul_pow_mem 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp Set Set.instMembership MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Finsupp.linearCombination AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.instHasSubset SetLike.coe Subalgebra instSetLike SetLike.instMembership Set.Elem Finsupp.instFunLike Algebra.toSMul Algebra.id Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	Subalgebra CommSemiring.toSemiring SetLike.instMembership instSetLike	—	mem_of_finset_sum_eq_one_of_pow_smul_mem

---

← Back to Index