Conjugation

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

Statistics

Metric	Count
Definitions `involute`, `involuteEquiv`, `reverse`, `reverseEquiv`, `reverseOp`, `reverseOpEquiv`	6
Theorems `evenOdd_comap_involute`, `evenOdd_comap_reverse`, `evenOdd_map_involute`, `evenOdd_map_reverse`, `involuteEquiv_apply`, `involuteEquiv_symm_apply`, `involute_comp_involute`, `involute_eq_of_mem_even`, `involute_eq_of_mem_odd`, `involute_involute`, `involute_involutive`, `involute_mem_evenOdd_iff`, `involute_prod_map_ι`, `involute_ι`, `op_reverse`, `commutes`, `map_mul`, `map_one`, `reverseEquiv_apply`, `reverseEquiv_symm_apply`, `reverseOpEquiv_apply`, `reverseOpEquiv_opComm`, `reverseOp_ι`, `reverse_comp_involute`, `reverse_comp_reverse`, `reverse_involute`, `reverse_involute_commute`, `reverse_involutive`, `reverse_mem_evenOdd_iff`, `reverse_prod_map_ι`, `reverse_reverse`, `reverse_ι`, `submodule_comap_mul_reverse`, `submodule_comap_pow_reverse`, `submodule_map_involute_eq_comap`, `submodule_map_mul_reverse`, `submodule_map_pow_reverse`, `submodule_map_reverse_eq_comap`, `unop_reverseOp`, `ι_range_comap_involute`, `ι_range_comap_reverse`, `ι_range_map_involute`, `ι_range_map_reverse`	43
Total	49

CliffordAlgebra

Definitions

Name	Category	Theorems
`involute` 📖	CompOp	33 math math: `involute_eq_of_mem_odd`, `CliffordAlgebraComplex.ofComplex_conj`, `involute_prod_map_ι`, `reverse_involute_commute`, `star_def'`, `toBaseChange_comp_involute`, `reverse_involute`, `star_def`, `involute_mem_evenOdd_iff`, `spinGroup.units_involute_act_eq_conjAct`, `coe_toEven_reverse_involute`, `spinGroup.involute_act_ι_mem_range_ι`, `involute_comp_involute`, `ι_range_map_involute`, `ι_range_comap_involute`, `involute_eq_of_mem_even`, `involute_ι`, `reverse_comp_involute`, `involute_involute`, `involuteEquiv_apply`, `CliffordAlgebraRing.involute_eq_id`, `evenOdd_map_involute`, `toBaseChange_involute`, `pinGroup.involute_act_ι_mem_range_ι`, `EquivEven.involute_e0`, `CliffordAlgebraComplex.toComplex_involute`, `involute_involutive`, `involuteEquiv_symm_apply`, `lipschitzGroup.involute_act_ι_mem_range_ι`, `evenOdd_comap_involute`, `spinGroup.involute_eq`, `EquivEven.involute_v`, `submodule_map_involute_eq_comap`
`involuteEquiv` 📖	CompOp	2 math math: `involuteEquiv_apply`, `involuteEquiv_symm_apply`
`reverse` 📖	CompOp	38 math math: `unop_reverseOp`, `toBaseChange_reverse`, `contractRight_eq`, `op_reverse`, `reverse_involute_commute`, `EquivEven.reverse_e0`, `star_def'`, `reverse_involute`, `star_def`, `coe_toEven_reverse_involute`, `reverse_comp_reverse`, `submodule_comap_mul_reverse`, `submodule_map_pow_reverse`, `evenOdd_map_reverse`, `ι_range_map_reverse`, `reverse.map_mul`, `reverse_prod_map_ι`, `reverse_reverse`, `foldl_reverse`, `reverse.commutes`, `reverse_mem_evenOdd_iff`, `foldr_reverse`, `reverse_comp_involute`, `reverseEquiv_symm_apply`, `submodule_map_mul_reverse`, `reverse.map_one`, `submodule_comap_pow_reverse`, `reverseEquiv_apply`, `CliffordAlgebraRing.reverse_apply`, `submodule_map_reverse_eq_comap`, `CliffordAlgebraComplex.reverse_eq_id`, `evenOdd_comap_reverse`, `EquivEven.reverse_v`, `CliffordAlgebraRing.reverse_eq_id`, `ι_range_comap_reverse`, `reverse_ι`, `reverse_involutive`, `CliffordAlgebraComplex.reverse_apply`
`reverseEquiv` 📖	CompOp	2 math math: `reverseEquiv_symm_apply`, `reverseEquiv_apply`
`reverseOp` 📖	CompOp	5 math math: `unop_reverseOp`, `op_reverse`, `toBaseChange_comp_reverseOp`, `reverseOp_ι`, `reverseOpEquiv_apply`
`reverseOpEquiv` 📖	CompOp	2 math math: `reverseOpEquiv_opComm`, `reverseOpEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`evenOdd_comap_involute` 📖	mathematical	—	`Submodule.comap` `CliffordAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `Algebra.toModule` `instAlgebraCliffordAlgebra` `RingHom.id` `AlgHom.toLinearMap` `involute` `evenOdd`	—	`RingHomSurjective.ids` `submodule_map_involute_eq_comap` `evenOdd_map_involute`
`evenOdd_comap_reverse` 📖	mathematical	—	`Submodule.comap` `CliffordAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `RingHom.id` `Semiring.toNonAssocSemiring` `reverse` `evenOdd`	—	`RingHomSurjective.ids` `submodule_map_reverse_eq_comap` `evenOdd_map_reverse`
`evenOdd_map_involute` 📖	mathematical	—	`Submodule.map` `CliffordAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `Algebra.toModule` `instAlgebraCliffordAlgebra` `RingHom.id` `RingHomSurjective.ids` `AlgHom.toLinearMap` `involute` `evenOdd`	—	`RingHomSurjective.ids` `Submodule.map_iSup` `IsScalarTower.right` `Submodule.map_pow` `ι_range_map_involute`
`evenOdd_map_reverse` 📖	mathematical	—	`Submodule.map` `CliffordAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `reverse` `evenOdd`	—	`RingHomSurjective.ids` `Submodule.map_iSup` `IsScalarTower.right` `submodule_map_pow_reverse` `ι_range_map_reverse`
`involuteEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `CliffordAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `instAlgebraCliffordAlgebra` `AlgEquiv.instFunLike` `involuteEquiv` `AlgHom` `AlgHom.funLike` `involute`	—	—
`involuteEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `CliffordAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `instAlgebraCliffordAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `involuteEquiv` `AlgHom` `AlgHom.funLike` `involute`	—	—
`involute_comp_involute` 📖	mathematical	—	`AlgHom.comp` `CliffordAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `instAlgebraCliffordAlgebra` `involute` `AlgHom.id`	—	`hom_ext` `LinearMap.ext` `RingHomCompTriple.ids` `involute_ι` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `neg_neg`
`involute_eq_of_mem_even` 📖	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`	`DFunLike.coe` `AlgHom` `AlgHom.funLike` `involute`	—	`even_induction` `AlgHom.commutes` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `involute_ι` `neg_mul_neg`
`involute_eq_of_mem_odd` 📖	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` `AlgHom` `AlgHom.funLike` `involute` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`odd_induction` `involute_ι` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `neg_add` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `neg_mul_neg` `mul_neg`
`involute_involute` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `CliffordAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `instAlgebraCliffordAlgebra` `AlgHom.funLike` `involute`	—	`involute_involutive`
`involute_involutive` 📖	mathematical	—	`Function.Involutive` `CliffordAlgebra` `DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `instAlgebraCliffordAlgebra` `AlgHom.funLike` `involute`	—	`AlgHom.congr_fun` `involute_comp_involute`
`involute_mem_evenOdd_iff` 📖	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` `DFunLike.coe` `AlgHom` `AlgHom.funLike` `involute`	—	`SetLike.ext_iff` `evenOdd_comap_involute`
`involute_prod_map_ι` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `CliffordAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `instAlgebraCliffordAlgebra` `AlgHom.funLike` `involute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `LinearMap.instFunLike` `ι` `Algebra.toSMul` `RingQuot.instSemiring` `TensorAlgebra` `instSemiringTensorAlgebra` `Rel` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `pow_zero` `one_smul` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `involute_ι` `Algebra.mul_smul_comm` `neg_mul` `smul_neg` `pow_succ` `mul_neg` `mul_one` `neg_smul`
`involute_ι` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `CliffordAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `instAlgebraCliffordAlgebra` `AlgHom.funLike` `involute` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `LinearMap.instFunLike` `ι` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`lift_ι_apply`
`op_reverse` 📖	mathematical	—	`MulOpposite.op` `CliffordAlgebra` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `reverse` `AlgHom` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `AlgHom.funLike` `reverseOp`	—	—
`reverseEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `CliffordAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `reverseEquiv` `LinearMap` `LinearMap.instFunLike` `reverse`	—	`RingHomInvPair.ids`
`reverseEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `CliffordAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `reverseEquiv` `LinearMap` `LinearMap.instFunLike` `reverse`	—	`RingHomInvPair.ids`
`reverseOpEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `CliffordAlgebra` `MulOpposite` `CommRing.toCommSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `MulOpposite.instSemiring` `instAlgebraCliffordAlgebra` `MulOpposite.instAlgebra` `AlgEquiv.instFunLike` `reverseOpEquiv` `AlgHom` `AlgHom.funLike` `reverseOp`	—	—
`reverseOpEquiv_opComm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AlgEquiv` `CliffordAlgebra` `MulOpposite` `CommRing.toCommSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `MulOpposite.instSemiring` `instAlgebraCliffordAlgebra` `MulOpposite.instAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `AlgEquiv.opComm` `reverseOpEquiv` `AlgEquiv.symm`	—	—
`reverseOp_ι` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `CliffordAlgebra` `MulOpposite` `CommRing.toCommSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `MulOpposite.instSemiring` `instAlgebraCliffordAlgebra` `MulOpposite.instAlgebra` `AlgHom.funLike` `reverseOp` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `LinearMap.instFunLike` `ι` `MulOpposite.op`	—	`lift_ι_apply`
`reverse_comp_involute` 📖	mathematical	—	`LinearMap.comp` `CliffordAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `instAlgebraCliffordAlgebra` `RingHom.id` `RingHomCompTriple.ids` `reverse` `AlgHom.toLinearMap` `involute`	—	`LinearMap.ext` `RingHomCompTriple.ids` `induction` `AlgHom.commutes` `reverse.commutes` `involute_ι` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `reverse_ι` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `reverse.map_mul` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `LinearMap.map_add`
`reverse_comp_reverse` 📖	mathematical	—	`LinearMap.comp` `CliffordAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `reverse` `LinearMap.id`	—	`LinearMap.ext` `RingHomCompTriple.ids` `reverse_involutive`
`reverse_involute` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CliffordAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `reverse` `AlgHom` `AlgHom.funLike` `involute`	—	`reverse_involute_commute`
`reverse_involute_commute` 📖	mathematical	—	`Function.Commute` `CliffordAlgebra` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `reverse` `AlgHom` `AlgHom.funLike` `involute`	—	`LinearMap.congr_fun` `RingHomCompTriple.ids` `reverse_comp_involute`
`reverse_involutive` 📖	mathematical	—	`Function.Involutive` `CliffordAlgebra` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `reverse`	—	`AlgHom.congr_fun` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `AlgEquiv.symm_comp`
`reverse_mem_evenOdd_iff` 📖	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` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `reverse`	—	`SetLike.ext_iff` `evenOdd_comap_reverse`
`reverse_prod_map_ι` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CliffordAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `reverse` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AddCommGroup.toAddCommMonoid` `ι`	—	`reverse.map_one` `reverse.map_mul` `reverse_ι` `Semigroup.to_isLawfulIdentity` `Semigroup.to_isAssociative` `mul_one`
`reverse_reverse` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CliffordAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `reverse`	—	`reverse_involutive`
`reverse_ι` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CliffordAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `reverse` `AddCommGroup.toAddCommMonoid` `ι`	—	`reverseOp_ι`
`submodule_comap_mul_reverse` 📖	mathematical	—	`Submodule.comap` `CliffordAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `RingHom.id` `Semiring.toNonAssocSemiring` `reverse` `Submodule` `Submodule.mul` `IsScalarTower.right` `RingQuot.instSemiring` `TensorAlgebra` `AddCommGroup.toAddCommMonoid` `instSemiringTensorAlgebra` `Rel`	—	`IsScalarTower.right` `RingHomSurjective.ids` `submodule_map_mul_reverse`
`submodule_comap_pow_reverse` 📖	mathematical	—	`Submodule.comap` `CliffordAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `RingHom.id` `Semiring.toNonAssocSemiring` `reverse` `Submodule` `Submodule.instPowNat` `IsScalarTower.right` `RingQuot.instSemiring` `TensorAlgebra` `AddCommGroup.toAddCommMonoid` `instSemiringTensorAlgebra` `Rel`	—	`IsScalarTower.right` `RingHomSurjective.ids` `submodule_map_pow_reverse`
`submodule_map_involute_eq_comap` 📖	mathematical	—	`Submodule.map` `CliffordAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `Algebra.toModule` `instAlgebraCliffordAlgebra` `RingHom.id` `RingHomSurjective.ids` `AlgHom.toLinearMap` `involute` `Submodule.comap`	—	`Submodule.map_equiv_eq_comap_symm` `RingHomInvPair.ids`
`submodule_map_mul_reverse` 📖	mathematical	—	`Submodule.map` `CliffordAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `reverse` `Submodule` `Submodule.mul` `IsScalarTower.right` `RingQuot.instSemiring` `TensorAlgebra` `AddCommGroup.toAddCommMonoid` `instSemiringTensorAlgebra` `Rel`	—	`RingHomSurjective.ids` `IsScalarTower.right` `Submodule.map_comp` `Submodule.map.congr_simp` `Submodule.map_mul` `RingHomInvPair.ids` `Submodule.map_unop_mul`
`submodule_map_pow_reverse` 📖	mathematical	—	`Submodule.map` `CliffordAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `reverse` `Submodule` `Submodule.instPowNat` `IsScalarTower.right` `RingQuot.instSemiring` `TensorAlgebra` `AddCommGroup.toAddCommMonoid` `instSemiringTensorAlgebra` `Rel`	—	`RingHomSurjective.ids` `IsScalarTower.right` `Submodule.map_comp` `Submodule.map.congr_simp` `Submodule.map_pow` `RingHomInvPair.ids` `Submodule.map_unop_pow`
`submodule_map_reverse_eq_comap` 📖	mathematical	—	`Submodule.map` `CliffordAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `reverse` `Submodule.comap`	—	`Submodule.map_equiv_eq_comap_symm` `RingHomInvPair.ids`
`unop_reverseOp` 📖	mathematical	—	`MulOpposite.unop` `CliffordAlgebra` `DFunLike.coe` `AlgHom` `MulOpposite` `CommRing.toCommSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `MulOpposite.instSemiring` `instAlgebraCliffordAlgebra` `MulOpposite.instAlgebra` `AlgHom.funLike` `reverseOp` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `LinearMap.instFunLike` `reverse`	—	—
`ι_range_comap_involute` 📖	mathematical	—	`Submodule.comap` `CliffordAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `Algebra.toModule` `instAlgebraCliffordAlgebra` `RingHom.id` `AlgHom.toLinearMap` `involute` `LinearMap.range` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `RingHomSurjective.ids` `ι`	—	`RingHomSurjective.ids` `submodule_map_involute_eq_comap` `ι_range_map_involute`
`ι_range_comap_reverse` 📖	mathematical	—	`Submodule.comap` `CliffordAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `RingHom.id` `Semiring.toNonAssocSemiring` `reverse` `LinearMap.range` `AddCommGroup.toAddCommMonoid` `RingHomSurjective.ids` `ι`	—	`RingHomSurjective.ids` `submodule_map_reverse_eq_comap` `ι_range_map_reverse`
`ι_range_map_involute` 📖	mathematical	—	`Submodule.map` `CliffordAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `Algebra.toModule` `instAlgebraCliffordAlgebra` `RingHom.id` `RingHomSurjective.ids` `AlgHom.toLinearMap` `involute` `LinearMap.range` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ι`	—	`RingHomSurjective.ids` `ι_range_map_lift` `LinearMap.range_neg`
`ι_range_map_reverse` 📖	mathematical	—	`Submodule.map` `CliffordAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `reverse` `LinearMap.range` `AddCommGroup.toAddCommMonoid` `ι`	—	`RingHomSurjective.ids` `reverse.eq_1` `reverseOp.eq_1` `Submodule.map_comp` `ι_range_map_lift` `LinearMap.range_comp` `RingHomCompTriple.ids` `Submodule.map_id`

CliffordAlgebra.reverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commutes` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CliffordAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `CliffordAlgebra.reverse` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`MulOpposite.op_injective` `AlgHom.commutes`
`map_mul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CliffordAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `CliffordAlgebra.reverse` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`MulOpposite.op_injective` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass`
`map_one` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CliffordAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `CliffordAlgebra.reverse` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`MulOpposite.op_injective` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`

---

← Back to Index