Grading

📁 Source: Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean

Statistics

Metric	Count
Definitions ι, evenOdd, gradedAlgebra	3
Theorems lift_ι_eq, ι_apply, ι_sq_scalar, gradedMonoid, evenOdd_induction, evenOdd_isCompl, evenOdd_mul_le, even_induction, iSup_ι_range_eq_top, odd_induction, one_le_evenOdd_zero, range_ι_le_evenOdd_one, ι_mem_evenOdd_one, ι_mul_ι_mem_evenOdd_zero	14
Total	17

CliffordAlgebra

Definitions

Name	Category	Theorems
evenOdd 📖	CompOp	24 math math: toProd_comp_ofProd, toProd_ι_tmul_one, evenOdd.gradedMonoid, involute_mem_evenOdd_iff, range_ι_le_evenOdd_one, one_le_evenOdd_zero, evenOdd_map_reverse, GradedAlgebra.ι_apply, ι_mul_ι_mem_evenOdd_zero, reverse_mem_evenOdd_iff, prodEquiv_symm_apply, even_toSubmodule, prodEquiv_apply, ofProd_comp_toProd, evenOdd_mul_le, evenOdd_map_involute, toProd_one_tmul_ι, ι_mem_evenOdd_one, evenOdd_comap_reverse, ofProd_ι_mk, GradedAlgebra.lift_ι_eq, evenOdd_comap_involute, GradedAlgebra.ι_sq_scalar, evenOdd_isCompl
gradedAlgebra 📖	CompOp	7 math math: toProd_comp_ofProd, toProd_ι_tmul_one, prodEquiv_symm_apply, prodEquiv_apply, ofProd_comp_toProd, toProd_one_tmul_ι, ofProd_ι_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
evenOdd_induction 📖	—	Submodule.mem_iSup_of_mem CliffordAlgebra CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra ZMod AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing Submodule Submodule.instPowNat LinearMap.range AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring ι ZMod.val ZMod.natCast_zmod_val Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Submodule.add_mem evenOdd Distrib.toMul DFunLike.coe LinearMap LinearMap.instFunLike AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddZero.toZero SetLike.instMembership Submodule.setLike SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero evenOdd.gradedMonoid ι_mul_ι_mem_evenOdd_zero zero_add	—	—	IsScalarTower.right RingHomSurjective.ids Submodule.mem_iSup_of_mem ZMod.natCast_zmod_val Submodule.add_mem SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul evenOdd.gradedMonoid ι_mul_ι_mem_evenOdd_zero zero_add Submodule.iSup_induction' add_comm pow_add pow_mul Submodule.mul_induction_on' Submodule.pow_induction_on_left' Submodule.mul_mem_mul Submodule.algebraMap_mem Submodule.smul_mem AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Submodule.addSubmonoidClass add_mul Distrib.rightDistribClass pow_succ' pow_two mul_assoc Submodule.zero_mem
evenOdd_isCompl 📖	mathematical	—	IsCompl Submodule CliffordAlgebra CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice evenOdd ZMod MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	DirectSum.IsInternal.isCompl zero_ne_one NeZero.one ZMod.nontrivial Nat.Prime.one_lt' Nat.fact_prime_two Finset.coe_univ Finset.coe_insert Finset.coe_singleton DirectSum.Decomposition.isInternal Submodule.addSubmonoidClass
evenOdd_mul_le 📖	mathematical	—	Submodule CliffordAlgebra CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.mul IsScalarTower.right RingQuot.instSemiring TensorAlgebra AddCommGroup.toAddCommMonoid instSemiringTensorAlgebra Rel evenOdd ZMod Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing	—	IsScalarTower.right Submodule.iSup_eq_span Submodule.span_mul_span Submodule.span_mono Set.iUnion_mul Set.mul_iUnion Set.mem_iUnion Nat.cast_add pow_add Submodule.mul_mem_mul
even_induction 📖	—	DFunLike.coe RingHom CliffordAlgebra Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra RingHom.instFunLike algebraMap instAlgebraCliffordAlgebra SetLike.algebraMap_mem_graded ZMod MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing evenOdd SetLike.GradedMonoid.toGradedOne Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule Submodule.setLike MonoidWithZero.toMonoid RingQuot TensorAlgebra AddCommGroup.toAddCommMonoid TensorAlgebra.instRing Rel RingQuot.instMonoidWithZero AddCommMonoid.toAddMonoid evenOdd.gradedMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Submodule.add_mem Distrib.toMul LinearMap RingHom.id LinearMap.instFunLike ι AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing AddZero.toZero SetLike.instMembership SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul Semiring.toMonoidWithZero ι_mul_ι_mem_evenOdd_zero zero_add	—	—	SetLike.algebraMap_mem_graded SetLike.GradedMonoid.toGradedOne evenOdd.gradedMonoid Submodule.add_mem SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul ι_mul_ι_mem_evenOdd_zero zero_add evenOdd_induction IsScalarTower.right RingHomSurjective.ids Submodule.mem_iSup_of_mem ZMod.natCast_zmod_val Submodule.mem_one
iSup_ι_range_eq_top 📖	mathematical	—	iSup Submodule CliffordAlgebra CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Submodule.instPowNat IsScalarTower.right RingQuot.instSemiring TensorAlgebra AddCommGroup.toAddCommMonoid instSemiringTensorAlgebra Rel LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ι Top.top Submodule.instTop	—	IsScalarTower.right RingHomSurjective.ids DirectSum.IsInternal.submodule_iSup_eq_top DirectSum.Decomposition.isInternal Submodule.addSubmonoidClass iSup_sigma Function.Surjective.iSup_congr
odd_induction 📖	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CliffordAlgebra AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike ι ι_mem_evenOdd_one Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Submodule.add_mem evenOdd ZMod AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing Distrib.toMul AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddZero.toZero Submodule SetLike.instMembership Submodule.setLike SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero evenOdd.gradedMonoid ι_mul_ι_mem_evenOdd_zero zero_add	—	—	ι_mem_evenOdd_one Submodule.add_mem SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul evenOdd.gradedMonoid ι_mul_ι_mem_evenOdd_zero zero_add evenOdd_induction IsScalarTower.right RingHomSurjective.ids Submodule.mem_iSup_of_mem ZMod.natCast_zmod_val ZMod.val_one Nat.Prime.one_lt' Nat.fact_prime_two pow_one
one_le_evenOdd_zero 📖	mathematical	—	Submodule CliffordAlgebra CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.one evenOdd ZMod MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing	—	le_trans Nat.cast_zero Eq.ge pow_zero le_iSup
range_ι_le_evenOdd_one 📖	mathematical	—	Submodule CliffordAlgebra CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LinearMap.range AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ι evenOdd ZMod AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing	—	le_trans RingHomSurjective.ids Nat.cast_one Eq.ge pow_one le_iSup
ι_mem_evenOdd_one 📖	mathematical	—	CliffordAlgebra Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike evenOdd ZMod AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike ι	—	range_ι_le_evenOdd_one LinearMap.mem_range_self RingHomSurjective.ids
ι_mul_ι_mem_evenOdd_zero 📖	mathematical	—	CliffordAlgebra Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike evenOdd ZMod MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike ι	—	Submodule.mem_iSup_of_mem pow_two Submodule.mul_mem_mul IsScalarTower.right LinearMap.mem_range_self RingHomSurjective.ids

CliffordAlgebra.GradedAlgebra

Definitions

Name	Category	Theorems
ι 📖	CompOp	3 math math: ι_apply, lift_ι_eq, ι_sq_scalar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift_ι_eq 📖	mathematical	—	DFunLike.coe AlgHom CliffordAlgebra DirectSum ZMod Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike CliffordAlgebra.evenOdd Submodule.addCommMonoid DirectSum.semiring ZMod.decidableEq AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing SetLike.gsemiring Submodule.addSubmonoidClass CliffordAlgebra.evenOdd.gradedMonoid DirectSum.instAlgebra Submodule.module Submodule.galgebra AlgHom.funLike Equiv LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike CliffordAlgebra.lift ι ι_sq_scalar AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum AddMonoidHom.instFunLike DirectSum.of	—	Submodule.addSubmonoidClass CliffordAlgebra.evenOdd.gradedMonoid ι_sq_scalar Submodule.iSup_induction' Submodule.mem_iSup_of_mem Submodule.pow_induction_on_left' Submodule.algebraMap_mem AlgHom.commutes DirectSum.algebraMap_apply IsScalarTower.right AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SetLike.GradedMonoid.toGradedMul map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass Submodule.mul_mem_mul pow_succ' map_mul NonUnitalAlgSemiHomClass.toMulHomClass CliffordAlgebra.lift_ι_apply CliffordAlgebra.ι_mem_evenOdd_one ι_apply DirectSum.of_mul_of DirectSum.of_eq_of_gradedMonoid_eq Sigma.subtype_ext add_comm Nat.cast_add Nat.cast_one ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass DFinsupp.single_eq_zero
ι_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring DirectSum ZMod CliffordAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike CliffordAlgebra.evenOdd Submodule.addCommMonoid AddCommGroup.toAddCommMonoid instAddCommMonoidDirectSum DirectSum.instModule Submodule.module LinearMap.instFunLike ι AddMonoidHom AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike DirectSum.of ZMod.decidableEq CliffordAlgebra.ι CliffordAlgebra.ι_mem_evenOdd_one	—	—
ι_sq_scalar 📖	mathematical	—	DirectSum ZMod CliffordAlgebra Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike CliffordAlgebra.evenOdd Submodule.addCommMonoid DirectSum.instMul ZMod.decidableEq Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing SetLike.gnonUnitalNonAssocSemiring Submodule.addSubmonoidClass SetLike.GradedMonoid.toGradedMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing CliffordAlgebra.evenOdd.gradedMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommMonoidDirectSum DirectSum.instModule Submodule.module LinearMap.instFunLike ι RingHom DirectSum.semiring SetLike.gsemiring RingHom.instFunLike algebraMap DirectSum.instAlgebra Submodule.galgebra QuadraticForm QuadraticMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	Submodule.addSubmonoidClass SetLike.GradedMonoid.toGradedMul CliffordAlgebra.evenOdd.gradedMonoid CliffordAlgebra.ι_mem_evenOdd_one ι_apply DirectSum.of_mul_of DirectSum.algebraMap_apply DirectSum.of_eq_of_gradedMonoid_eq Sigma.subtype_ext CliffordAlgebra.ι_sq_scalar

CliffordAlgebra.evenOdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gradedMonoid 📖	mathematical	—	SetLike.GradedMonoid ZMod CliffordAlgebra Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra Submodule.setLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing CliffordAlgebra.evenOdd	—	Submodule.one_le CliffordAlgebra.one_le_evenOdd_zero IsScalarTower.right Submodule.mul_le CliffordAlgebra.evenOdd_mul_le

---

← Back to Index