Documentation Verification Report

BaseChange

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

Statistics

Metric	Count
Definitions `equivBaseChange`, `ofBaseChange`, `ofBaseChangeAux`, `toBaseChange`	4
Theorems `equivBaseChange_apply`, `equivBaseChange_symm_apply`, `ofBaseChangeAux_ι`, `ofBaseChange_comp_toBaseChange`, `ofBaseChange_tmul_one`, `ofBaseChange_tmul_ι`, `ofBaseChange_toBaseChange`, `toBaseChange_comp_involute`, `toBaseChange_comp_ofBaseChange`, `toBaseChange_comp_reverseOp`, `toBaseChange_involute`, `toBaseChange_ofBaseChange`, `toBaseChange_reverse`, `toBaseChange_ι`	14
Total	18

CliffordAlgebra

Definitions

Name	Category	Theorems
`equivBaseChange` 📖	CompOp	2 math math: `equivBaseChange_symm_apply`, `equivBaseChange_apply`
`ofBaseChange` 📖	CompOp	7 math math: `equivBaseChange_symm_apply`, `ofBaseChange_toBaseChange`, `toBaseChange_comp_ofBaseChange`, `ofBaseChange_tmul_ι`, `toBaseChange_ofBaseChange`, `ofBaseChange_tmul_one`, `ofBaseChange_comp_toBaseChange`
`ofBaseChangeAux` 📖	CompOp	1 math math: `ofBaseChangeAux_ι`
`toBaseChange` 📖	CompOp	10 math math: `toBaseChange_reverse`, `ofBaseChange_toBaseChange`, `toBaseChange_comp_ofBaseChange`, `toBaseChange_comp_involute`, `toBaseChange_ofBaseChange`, `toBaseChange_comp_reverseOp`, `equivBaseChange_apply`, `toBaseChange_involute`, `toBaseChange_ι`, `ofBaseChange_comp_toBaseChange`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivBaseChange_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `CliffordAlgebra` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `QuadraticForm.baseChange` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `equivBaseChange` `AlgHom` `AlgHom.funLike` `toBaseChange`	—	`Nat.instAtLeastTwoHAddOfNat` `Algebra.to_smulCommClass`
`equivBaseChange_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `CommRing.toCommSemiring` `CliffordAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `CommSemiring.toSemiring` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `QuadraticForm.baseChange` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `AlgEquiv.symm` `equivBaseChange` `AlgHom` `AlgHom.funLike` `ofBaseChange`	—	`Nat.instAtLeastTwoHAddOfNat` `Algebra.to_smulCommClass`
`ofBaseChangeAux_ι` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `CliffordAlgebra` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `QuadraticForm.baseChange` `Ring.toSemiring` `instRingCliffordAlgebra` `instAlgebraCliffordAlgebra` `instAlgebra'` `TensorProduct.instModule` `TensorProduct.isScalarTower_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `IsScalarTower.right` `AlgHom.funLike` `ofBaseChangeAux` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `LinearMap.instFunLike` `ι` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Nat.instAtLeastTwoHAddOfNat` `lift_ι_apply` `Algebra.to_smulCommClass`
`ofBaseChange_comp_toBaseChange` 📖	mathematical	—	`AlgHom.comp` `CliffordAlgebra` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `QuadraticForm.baseChange` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `ofBaseChange` `toBaseChange` `AlgHom.id`	—	`Nat.instAtLeastTwoHAddOfNat` `hom_ext` `Algebra.to_smulCommClass` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.right` `TensorProduct.isScalarTower_left` `instIsScalarTower` `IsScalarTower.left` `RingHomCompTriple.ids` `LinearMap.ext_ring` `IsScalarTower.to_smulCommClass` `LinearMap.ext` `toBaseChange_ι` `ofBaseChange_tmul_ι`
`ofBaseChange_tmul_one` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `TensorProduct` `CommRing.toCommSemiring` `CliffordAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `CommSemiring.toSemiring` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `QuadraticForm.baseChange` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `AlgHom.funLike` `ofBaseChange` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`Nat.instAtLeastTwoHAddOfNat` `Algebra.to_smulCommClass` `TensorProduct.isScalarTower_left` `IsScalarTower.right` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `mul_one`
`ofBaseChange_tmul_ι` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `TensorProduct` `CommRing.toCommSemiring` `CliffordAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `CommSemiring.toSemiring` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `QuadraticForm.baseChange` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `AlgHom.funLike` `ofBaseChange` `TensorProduct.tmul` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `ι`	—	`Nat.instAtLeastTwoHAddOfNat` `Algebra.to_smulCommClass` `TensorProduct.isScalarTower_left` `IsScalarTower.right` `ofBaseChangeAux_ι` `Algebra.smul_def` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `TensorProduct.smul_tmul'` `smul_eq_mul` `mul_one`
`ofBaseChange_toBaseChange` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `TensorProduct` `CommRing.toCommSemiring` `CliffordAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `CommSemiring.toSemiring` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `QuadraticForm.baseChange` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `AlgHom.funLike` `ofBaseChange` `toBaseChange`	—	`Nat.instAtLeastTwoHAddOfNat` `Algebra.to_smulCommClass` `AlgHom.congr_fun` `ofBaseChange_comp_toBaseChange`
`toBaseChange_comp_involute` 📖	mathematical	—	`AlgHom.comp` `CliffordAlgebra` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `QuadraticForm.baseChange` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `toBaseChange` `involute` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `Algebra.TensorProduct.map` `AlgHom.id`	—	`Nat.instAtLeastTwoHAddOfNat` `hom_ext` `Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `TensorProduct.AlgebraTensorModule.curry_injective` `TensorProduct.isScalarTower_left` `RingHomCompTriple.ids` `LinearMap.ext_ring` `LinearMap.ext` `toBaseChange_ι` `involute_ι` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Algebra.TensorProduct.map_tmul` `AlgHom.id_apply` `TensorProduct.tmul_neg`
`toBaseChange_comp_ofBaseChange` 📖	mathematical	—	`AlgHom.comp` `TensorProduct` `CommRing.toCommSemiring` `CliffordAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `CommSemiring.toSemiring` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `QuadraticForm.baseChange` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `toBaseChange` `ofBaseChange` `AlgHom.id`	—	`Nat.instAtLeastTwoHAddOfNat` `Algebra.TensorProduct.ext` `Algebra.to_smulCommClass` `IsScalarTower.right` `TensorProduct.isScalarTower_left` `Algebra.ext_id` `IsScalarTower.to_smulCommClass` `hom_ext` `LinearMap.ext` `RingHomCompTriple.ids` `ofBaseChange_tmul_ι` `toBaseChange_ι` `CompTriple.comp_eq` `CompTriple.instId_comp` `CompTriple.instIsIdId`
`toBaseChange_comp_reverseOp` 📖	mathematical	—	`AlgHom.comp` `CliffordAlgebra` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `QuadraticForm.baseChange` `MulOpposite` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `MulOpposite.instSemiring` `Algebra.TensorProduct.instSemiring` `MulOpposite.instAlgebra` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `DFunLike.coe` `Equiv` `AlgHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `AlgHom.op` `toBaseChange` `reverseOp` `MulOpposite.instAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulOpposite.instModule` `MulOpposite.instSMulCommClass` `Algebra.toSMul` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `AlgEquiv.toAlgHom` `Algebra.TensorProduct.opAlgEquiv` `MulOpposite.instIsScalarTower` `Algebra.TensorProduct.map` `AlgEquiv.toOpposite`	—	`Nat.instAtLeastTwoHAddOfNat` `hom_ext` `Algebra.to_smulCommClass` `MulOpposite.instSMulCommClass` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `MulOpposite.instIsScalarTower` `TensorProduct.AlgebraTensorModule.curry_injective` `TensorProduct.isScalarTower_left` `RingHomCompTriple.ids` `LinearMap.ext_ring` `LinearMap.ext` `toBaseChange_ι` `reverse_ι` `Algebra.TensorProduct.map_tmul` `Algebra.TensorProduct.opAlgEquiv_tmul` `reverseOp_ι`
`toBaseChange_involute` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `CliffordAlgebra` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `QuadraticForm.baseChange` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `AlgHom.funLike` `toBaseChange` `involute` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `TensorProduct.map` `LinearMap.id` `AlgHom.toLinearMap`	—	`Nat.instAtLeastTwoHAddOfNat` `Algebra.to_smulCommClass` `DFunLike.congr_fun` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `toBaseChange_comp_involute`
`toBaseChange_ofBaseChange` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `CliffordAlgebra` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `QuadraticForm.baseChange` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `AlgHom.funLike` `toBaseChange` `ofBaseChange`	—	`Nat.instAtLeastTwoHAddOfNat` `AlgHom.congr_fun` `Algebra.to_smulCommClass` `toBaseChange_comp_ofBaseChange`
`toBaseChange_reverse` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `CliffordAlgebra` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `QuadraticForm.baseChange` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `AlgHom.funLike` `toBaseChange` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `reverse` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.map` `LinearMap.id`	—	`Nat.instAtLeastTwoHAddOfNat` `Algebra.to_smulCommClass` `MulOpposite.instSMulCommClass` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `MulOpposite.instIsScalarTower` `DFunLike.congr_fun` `toBaseChange_comp_reverseOp` `RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearMap.congr_fun` `TensorProduct.AlgebraTensorModule.map_comp` `reverse.eq_1` `AlgEquiv.toLinearMap.eq_1` `AlgEquiv.toLinearEquiv_toLinearMap` `AlgEquiv.toLinearEquiv_toOpposite` `RingHomInvPair.triples₂` `LinearEquiv.self_trans_symm`
`toBaseChange_ι` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `CliffordAlgebra` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `QuadraticForm.baseChange` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `AlgHom.funLike` `toBaseChange` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `ι` `TensorProduct.tmul`	—	`Nat.instAtLeastTwoHAddOfNat` `lift_ι_apply`

---

← Back to Index