Defs

📁 Source: Mathlib/Algebra/QuadraticAlgebra/Defs.lean

Statistics

Metric	Count
Definitions `C`, `basis`, `equivProd`, `im`, `imₗ`, `instAdd`, `instAddCommGroup`, `instAddCommGroupWithOne`, `instAddCommMonoid`, `instAddCommMonoidWithOne`, `instAddGroup`, `instAddMonoid`, `instAlgebra`, `instCommRing`, `instCommSemiring`, `instDistribMulAction`, `instInhabited`, `instModule`, `instMul`, `instMulAction`, `instNeg`, `instNonAssocSemiring`, `instNonUnitalNonAssocSemiring`, `instOne`, `instSMul`, `instSub`, `instZero`, `linearEquivTuple`, `re`, `reₗ`, `instDecidableEqQuadraticAlgebra`, `decEq`	32
Theorems `C_add`, `C_eq_algebraMap`, `C_eq_one_iff`, `C_eq_zero_iff`, `C_inj`, `C_injective`, `C_intCast`, `C_mul`, `C_mul_eq_smul`, `C_natCast`, `C_neg`, `C_ofNat`, `C_one`, `C_pow`, `C_smul`, `C_sub`, `C_zero`, `algebraMap_dvd_iff`, `algebraMap_dvd_iff_dvd`, `algebraMap_eq`, `algebraMap_im`, `algebraMap_inj`, `algebraMap_injective`, `algebraMap_re`, `basis_repr_apply`, `coe_add`, `coe_algebraMap`, `coe_dvd_iff`, `coe_dvd_iff_dvd`, `coe_eq_one_iff`, `coe_eq_zero_iff`, `coe_inj`, `coe_injective`, `coe_intCast`, `coe_mul`, `coe_mul_eq_smul`, `coe_natCast`, `coe_neg`, `coe_ofNat`, `coe_one`, `coe_pow`, `coe_smul`, `coe_sub`, `coe_zero`, `equivProd_symm_apply`, `ext`, `ext_iff`, `finrank_eq_two`, `im_C`, `im_add`, `im_coe`, `im_intCast`, `im_mul`, `im_natCast`, `im_neg`, `im_ofNat`, `im_one`, `im_smul`, `im_sub`, `im_zero`, `imₗ_apply`, `instCharZero`, `instFinite`, `instFree`, `instIsCentralScalar`, `instIsScalarTower`, `instIsTorsionFree`, `instNontrivial`, `instSMulCommClass`, `instSubsingleton`, `linearEquivTuple_apply`, `linearEquivTuple_symm_apply`, `mk_add_mk`, `mk_eta`, `mk_mul_mk`, `mk_sub_mk`, `mul_C_eq_smul`, `mul_coe_eq_smul`, `neg_mk`, `nsmul_mk`, `rank_eq_two`, `re_C`, `re_add`, `re_coe`, `re_intCast`, `re_mul`, `re_natCast`, `re_neg`, `re_ofNat`, `re_one`, `re_smul`, `re_sub`, `re_zero`, `reₗ_apply`, `smul_C`, `smul_coe`, `smul_mk`, `zsmul_val`	98
Total	130

QuadraticAlgebra

Definitions

Name	Category	Theorems
`C` 📖	CompOp	42 math math: `coe_sub`, `coe_mul_eq_smul`, `C_eq_zero_iff`, `C_pow`, `coe_one`, `coe_mul`, `C_add`, `mul_coe_eq_smul`, `C_eq_algebraMap`, `C_mul`, `coe_eq_one_iff`, `C_sub`, `C_eq_one_iff`, `C_neg`, `C_natCast`, `im_C`, `coe_neg`, `smul_C`, `C_injective`, `C_intCast`, `coe_inj`, `C_mul_eq_smul`, `coe_natCast`, `smul_coe`, `coe_ofNat`, `coe_add`, `C_ofNat`, `C_one`, `coe_pow`, `mul_C_eq_smul`, `coe_intCast`, `im_coe`, `re_coe`, `C_smul`, `coe_algebraMap`, `coe_injective`, `C_inj`, `coe_eq_zero_iff`, `C_zero`, `re_C`, `coe_zero`, `coe_smul`
`basis` 📖	CompOp	1 math math: `basis_repr_apply`
`equivProd` 📖	CompOp	1 math math: `equivProd_symm_apply`
`im` 📖	CompOp	27 math math: `im_intCast`, `mk_add_mk`, `linearEquivTuple_apply`, `algebraMap_dvd_iff`, `imₗ_apply`, `im_ofNat`, `lift_apply_apply`, `im_C`, `im_smul`, `mk_eta`, `im_neg`, `basis_repr_apply`, `re_star`, `im_one`, `im_mul`, `im_zero`, `norm_def`, `omega_im`, `im_coe`, `im_sub`, `re_mul`, `im_natCast`, `im_add`, `im_star`, `ext_iff`, `coe_dvd_iff`, `algebraMap_im`
`imₗ` 📖	CompOp	1 math math: `imₗ_apply`
`instAdd` 📖	CompOp	8 math math: `mk_add_mk`, `C_add`, `mul_star`, `coe_add`, `mk_eq_add_smul_omega`, `re_add`, `omega_mul_omega_eq_add`, `im_add`
`instAddCommGroup` 📖	CompOp	1 math math: `det_toLinearMap_eq_norm`
`instAddCommGroupWithOne` 📖	CompOp	4 math math: `im_intCast`, `C_intCast`, `coe_intCast`, `re_intCast`
`instAddCommMonoid` 📖	CompOp	11 math math: `linearEquivTuple_apply`, `instFinite`, `imₗ_apply`, `instFree`, `reₗ_apply`, `rank_eq_two`, `basis_repr_apply`, `linearEquivTuple_symm_apply`, `instIsTorsionFree`, `finrank_eq_two`, `det_toLinearMap_eq_norm`
`instAddCommMonoidWithOne` 📖	CompOp	5 math math: `nsmul_mk`, `C_natCast`, `coe_natCast`, `re_natCast`, `im_natCast`
`instAddGroup` 📖	CompOp	—
`instAddMonoid` 📖	CompOp	—
`instAlgebra` 📖	CompOp	25 math math: `algebraMap_inj`, `norm_algebraMap`, `algebraMap_re`, `omega_mul_coe_mul_mk`, `algebraMap_dvd_iff`, `C_eq_algebraMap`, `lift_apply_apply`, `coe_dvd_iff_dvd`, `mul_star`, `norm_coe`, `coe_norm_eq_mul_star`, `algebraMap_eq`, `lift_symm_apply_coe`, `omega_mul_algebraMap_mul_mk`, `algHom_ext_iff`, `algebraMap_dvd_iff_dvd`, `mk_eq_add_smul_omega`, `coe_mem_nonZeroDivisors_iff`, `algebraMap_norm_eq_mul_star`, `algebraMap_mem_nonZeroDivisors_iff`, `coe_algebraMap`, `det_toLinearMap_eq_norm`, `coe_dvd_iff`, `algebraMap_im`, `algebraMap_injective`
`instCommRing` 📖	CompOp	4 math math: `zsmul_val`, `norm_natCast`, `norm_intCast`, `instCharZero`
`instCommSemiring` 📖	CompOp	33 math math: `C_pow`, `algebraMap_inj`, `norm_algebraMap`, `algebraMap_re`, `omega_mul_coe_mul_mk`, `algebraMap_dvd_iff`, `C_eq_algebraMap`, `norm_eq_one_iff_mem_unitary`, `lift_apply_apply`, `star_mem_nonZeroDivisors_iff`, `mem_unitary`, `coe_dvd_iff_dvd`, `mul_star`, `norm_coe`, `isUnit_iff_norm_isUnit`, `coe_norm_eq_mul_star`, `algebraMap_eq`, `lift_symm_apply_coe`, `mker_norm_eq_unitary`, `omega_mul_algebraMap_mul_mk`, `coe_pow`, `algHom_ext_iff`, `algebraMap_dvd_iff_dvd`, `mk_eq_add_smul_omega`, `coe_mem_nonZeroDivisors_iff`, `algebraMap_norm_eq_mul_star`, `algebraMap_mem_nonZeroDivisors_iff`, `coe_algebraMap`, `det_toLinearMap_eq_norm`, `norm_mem_nonZeroDivisors_iff`, `coe_dvd_iff`, `algebraMap_im`, `algebraMap_injective`
`instDistribMulAction` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instModule` 📖	CompOp	11 math math: `linearEquivTuple_apply`, `instFinite`, `imₗ_apply`, `instFree`, `reₗ_apply`, `rank_eq_two`, `basis_repr_apply`, `linearEquivTuple_symm_apply`, `instIsTorsionFree`, `finrank_eq_two`, `det_toLinearMap_eq_norm`
`instMul` 📖	CompOp	19 math math: `coe_mul_eq_smul`, `coe_mul`, `zsmul_val`, `nsmul_mk`, `omega_mul_coe_mul_mk`, `mul_coe_eq_smul`, `C_mul`, `mul_star`, `C_mul_eq_smul`, `coe_norm_eq_mul_star`, `omega_mul_omega_eq_mk`, `im_mul`, `mk_mul_mk`, `omega_mul_algebraMap_mul_mk`, `mul_C_eq_smul`, `algebraMap_norm_eq_mul_star`, `re_mul`, `omega_mul_mk`, `omega_mul_omega_eq_add`
`instMulAction` 📖	CompOp	—
`instNeg` 📖	CompOp	6 math math: `neg_mk`, `norm_neg`, `C_neg`, `coe_neg`, `im_neg`, `re_neg`
`instNonAssocSemiring` 📖	CompOp	18 math math: `norm_algebraMap`, `norm_zero`, `norm_eq_one_iff_mem_unitary`, `norm_eq_one`, `norm_neg`, `norm_natCast`, `norm_coe`, `isUnit_iff_norm_isUnit`, `coe_norm_eq_mul_star`, `norm_intCast`, `mker_norm_eq_unitary`, `norm_def`, `norm_one`, `norm_star`, `algebraMap_norm_eq_mul_star`, `det_toLinearMap_eq_norm`, `norm_mem_nonZeroDivisors_iff`, `norm_eq_zero_iff_eq_zero`
`instNonUnitalNonAssocSemiring` 📖	CompOp	1 math math: `det_toLinearMap_eq_norm`
`instOne` 📖	CompOp	8 math math: `coe_one`, `coe_eq_one_iff`, `C_eq_one_iff`, `im_one`, `C_one`, `norm_one`, `re_one`, `omega_mul_omega_eq_add`
`instSMul` 📖	CompOp	16 math math: `instIsScalarTower`, `coe_mul_eq_smul`, `mul_coe_eq_smul`, `smul_C`, `im_smul`, `C_mul_eq_smul`, `smul_coe`, `re_smul`, `instSMulCommClass`, `mul_C_eq_smul`, `mk_eq_add_smul_omega`, `C_smul`, `smul_mk`, `omega_mul_omega_eq_add`, `instIsCentralScalar`, `coe_smul`
`instSub` 📖	CompOp	6 math math: `coe_sub`, `C_sub`, `mul_star`, `mk_sub_mk`, `re_sub`, `im_sub`
`instZero` 📖	CompOp	8 math math: `C_eq_zero_iff`, `norm_zero`, `re_zero`, `im_zero`, `coe_eq_zero_iff`, `C_zero`, `norm_eq_zero_iff_eq_zero`, `coe_zero`
`linearEquivTuple` 📖	CompOp	2 math math: `linearEquivTuple_apply`, `linearEquivTuple_symm_apply`
`re` 📖	CompOp	26 math math: `mk_add_mk`, `linearEquivTuple_apply`, `algebraMap_re`, `algebraMap_dvd_iff`, `re_zero`, `lift_apply_apply`, `reₗ_apply`, `mk_eta`, `re_ofNat`, `basis_repr_apply`, `re_neg`, `re_star`, `omega_re`, `re_smul`, `im_mul`, `norm_def`, `re_sub`, `re_natCast`, `re_coe`, `re_add`, `re_one`, `re_mul`, `re_C`, `ext_iff`, `coe_dvd_iff`, `re_intCast`
`reₗ` 📖	CompOp	1 math math: `reₗ_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C_add` 📖	mathematical	—	`C` `AddZero.toZero` `AddZeroClass.toAddZero` `AddZero.toAdd` `QuadraticAlgebra` `instAdd`	—	`ext` `add_zero`
`C_eq_algebraMap` 📖	mathematical	—	`C` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `QuadraticAlgebra` `instCommSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Algebra.id`	—	—
`C_eq_one_iff` 📖	mathematical	—	`C` `QuadraticAlgebra` `instOne`	—	`C_one`
`C_eq_zero_iff` 📖	mathematical	—	`C` `QuadraticAlgebra` `instZero`	—	`C_zero`
`C_inj` 📖	mathematical	—	`C`	—	`C_injective`
`C_injective` 📖	mathematical	—	`QuadraticAlgebra` `C`	—	—
`C_intCast` 📖	mathematical	—	`C` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddCommGroupWithOne.toAddCommGroup` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `QuadraticAlgebra` `instAddCommGroupWithOne`	—	—
`C_mul` 📖	mathematical	—	`C` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `QuadraticAlgebra` `instMul` `Distrib.toAdd`	—	`ext` `MulZeroClass.mul_zero` `add_zero` `MulZeroClass.zero_mul`
`C_mul_eq_smul` 📖	mathematical	—	`QuadraticAlgebra` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toAdd` `C` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `instDistribSMul`	—	`ext` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `add_zero`
`C_natCast` 📖	mathematical	—	`C` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toNatCast` `QuadraticAlgebra` `instAddCommMonoidWithOne`	—	—
`C_neg` 📖	mathematical	—	`C` `NegZeroClass.toZero` `NegZeroClass.toNeg` `QuadraticAlgebra` `instNeg`	—	`ext` `neg_zero`
`C_ofNat` 📖	mathematical	—	`C` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne`	—	`ext`
`C_one` 📖	mathematical	—	`C` `QuadraticAlgebra` `instOne`	—	—
`C_pow` 📖	mathematical	—	`C` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `QuadraticAlgebra` `instCommSemiring`	—	`RingHom.map_pow`
`C_smul` 📖	mathematical	—	`C` `SMulZeroClass.toSMul` `QuadraticAlgebra` `instSMul`	—	`ext` `smul_zero`
`C_sub` 📖	mathematical	—	`C` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubNegMonoid.toSub` `SubNegZeroMonoid.toSubNegMonoid` `QuadraticAlgebra` `instSub`	—	`ext` `zero_sub_zero`
`C_zero` 📖	mathematical	—	`C` `QuadraticAlgebra` `instZero`	—	—
`algebraMap_dvd_iff` 📖	mathematical	—	`QuadraticAlgebra` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `instCommSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Algebra.id` `re` `im`	—	`MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `add_zero`
`algebraMap_dvd_iff_dvd` 📖	mathematical	—	`QuadraticAlgebra` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `instCommSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Algebra.id`	—	`algebraMap_dvd_iff`
`algebraMap_eq` 📖	mathematical	—	`DFunLike.coe` `RingHom` `QuadraticAlgebra` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Algebra.id` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	—
`algebraMap_im` 📖	mathematical	—	`im` `DFunLike.coe` `RingHom` `QuadraticAlgebra` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Algebra.id` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	—
`algebraMap_inj` 📖	mathematical	—	`DFunLike.coe` `RingHom` `QuadraticAlgebra` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Algebra.id`	—	`algebraMap_injective`
`algebraMap_injective` 📖	mathematical	—	`QuadraticAlgebra` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Algebra.id`	—	—
`algebraMap_re` 📖	mathematical	—	`re` `DFunLike.coe` `RingHom` `QuadraticAlgebra` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Algebra.id`	—	—
`basis_repr_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `QuadraticAlgebra` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.instAddCommMonoid` `instModule` `Semiring.toModule` `Finsupp.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `basis` `Matrix.vecCons` `re` `im` `Matrix.vecEmpty`	—	`RingHomInvPair.ids`
`coe_add` 📖	mathematical	—	`C` `AddZero.toZero` `AddZeroClass.toAddZero` `AddZero.toAdd` `QuadraticAlgebra` `instAdd`	—	`C_add`
`coe_algebraMap` 📖	mathematical	—	`C` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `QuadraticAlgebra` `instCommSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Algebra.id`	—	`C_eq_algebraMap`
`coe_dvd_iff` 📖	mathematical	—	`QuadraticAlgebra` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `instCommSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Algebra.id` `re` `im`	—	`algebraMap_dvd_iff`
`coe_dvd_iff_dvd` 📖	mathematical	—	`QuadraticAlgebra` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `instCommSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Algebra.id`	—	`algebraMap_dvd_iff_dvd`
`coe_eq_one_iff` 📖	mathematical	—	`C` `QuadraticAlgebra` `instOne`	—	`C_eq_one_iff`
`coe_eq_zero_iff` 📖	mathematical	—	`C` `QuadraticAlgebra` `instZero`	—	`C_eq_zero_iff`
`coe_inj` 📖	mathematical	—	`C`	—	—
`coe_injective` 📖	mathematical	—	`QuadraticAlgebra` `C`	—	`C_injective`
`coe_intCast` 📖	mathematical	—	`C` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddCommGroupWithOne.toAddCommGroup` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `QuadraticAlgebra` `instAddCommGroupWithOne`	—	`C_intCast`
`coe_mul` 📖	mathematical	—	`C` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `QuadraticAlgebra` `instMul` `Distrib.toAdd`	—	`C_mul`
`coe_mul_eq_smul` 📖	mathematical	—	`QuadraticAlgebra` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toAdd` `C` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `instDistribSMul`	—	`C_mul_eq_smul`
`coe_natCast` 📖	mathematical	—	`C` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toNatCast` `QuadraticAlgebra` `instAddCommMonoidWithOne`	—	`C_natCast`
`coe_neg` 📖	mathematical	—	`C` `NegZeroClass.toZero` `NegZeroClass.toNeg` `QuadraticAlgebra` `instNeg`	—	`C_neg`
`coe_ofNat` 📖	mathematical	—	`C` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne`	—	`C_ofNat`
`coe_one` 📖	mathematical	—	`C` `QuadraticAlgebra` `instOne`	—	`C_one`
`coe_pow` 📖	mathematical	—	`C` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `QuadraticAlgebra` `instCommSemiring`	—	`C_pow`
`coe_smul` 📖	mathematical	—	`C` `SMulZeroClass.toSMul` `QuadraticAlgebra` `instSMul`	—	`C_smul`
`coe_sub` 📖	mathematical	—	`C` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubNegMonoid.toSub` `SubNegZeroMonoid.toSubNegMonoid` `QuadraticAlgebra` `instSub`	—	`C_sub`
`coe_zero` 📖	mathematical	—	`C` `QuadraticAlgebra` `instZero`	—	`C_zero`
`equivProd_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `QuadraticAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivProd`	—	—
`ext` 📖	—	`re` `im`	—	—	—
`ext_iff` 📖	mathematical	—	`re` `im`	—	`ext`
`finrank_eq_two` 📖	mathematical	—	`Module.finrank` `QuadraticAlgebra` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instModule` `Semiring.toModule`	—	`Nat.instAtLeastTwoHAddOfNat` `rank_eq_two` `Cardinal.toNat_ofNat`
`im_C` 📖	mathematical	—	`im` `C`	—	—
`im_add` 📖	mathematical	—	`im` `QuadraticAlgebra` `instAdd`	—	—
`im_coe` 📖	mathematical	—	`im` `C`	—	`im_C`
`im_intCast` 📖	mathematical	—	`im` `QuadraticAlgebra` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `instAddCommGroupWithOne` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddCommGroupWithOne.toAddCommGroup`	—	—
`im_mul` 📖	mathematical	—	`im` `QuadraticAlgebra` `instMul` `re`	—	—
`im_natCast` 📖	mathematical	—	`im` `QuadraticAlgebra` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid`	—	—
`im_neg` 📖	mathematical	—	`im` `QuadraticAlgebra` `instNeg`	—	—
`im_ofNat` 📖	mathematical	—	`im` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne`	—	—
`im_one` 📖	mathematical	—	`im` `QuadraticAlgebra` `instOne`	—	—
`im_smul` 📖	mathematical	—	`im` `QuadraticAlgebra` `instSMul`	—	—
`im_sub` 📖	mathematical	—	`im` `QuadraticAlgebra` `instSub`	—	—
`im_zero` 📖	mathematical	—	`im` `QuadraticAlgebra` `instZero`	—	—
`imₗ_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `QuadraticAlgebra` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `imₗ` `im`	—	—
`instCharZero` 📖	mathematical	—	`CharZero` `QuadraticAlgebra` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing`	—	—
`instFinite` 📖	mathematical	—	`Module.Finite` `QuadraticAlgebra` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instModule` `Semiring.toModule`	—	`Module.Finite.of_basis` `Finite.of_fintype`
`instFree` 📖	mathematical	—	`Module.Free` `QuadraticAlgebra` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instModule` `Semiring.toModule`	—	`Module.Free.of_basis`
`instIsCentralScalar` 📖	mathematical	—	`IsCentralScalar` `QuadraticAlgebra` `instSMul` `MulOpposite`	—	`ext` `IsCentralScalar.op_smul_eq_smul`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `QuadraticAlgebra` `instSMul`	—	`ext` `smul_assoc`
`instIsTorsionFree` 📖	mathematical	—	`Module.IsTorsionFree` `QuadraticAlgebra` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instModule`	—	`Function.Injective.moduleIsTorsionFree` `Pi.instModuleIsTorsionFree` `RingHomInvPair.ids` `LinearEquiv.injective` `Matrix.smul_cons` `Matrix.smul_empty`
`instNontrivial` 📖	mathematical	—	`Nontrivial` `QuadraticAlgebra`	—	`Equiv.nontrivial` `nontrivial_prod_left` `Nontrivial.to_nonempty`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `QuadraticAlgebra` `instSMul`	—	`ext` `SMulCommClass.smul_comm`
`instSubsingleton` 📖	mathematical	—	`QuadraticAlgebra`	—	`Equiv.subsingleton`
`linearEquivTuple_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `QuadraticAlgebra` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.addCommMonoid` `instModule` `Semiring.toModule` `Pi.Function.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `linearEquivTuple` `Matrix.vecCons` `re` `im` `Matrix.vecEmpty`	—	`RingHomInvPair.ids`
`linearEquivTuple_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `QuadraticAlgebra` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `Pi.Function.module` `Semiring.toModule` `instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `linearEquivTuple`	—	`RingHomInvPair.ids`
`mk_add_mk` 📖	mathematical	—	`QuadraticAlgebra` `instAdd` `re` `im`	—	—
`mk_eta` 📖	mathematical	—	`re` `im`	—	—
`mk_mul_mk` 📖	mathematical	—	`QuadraticAlgebra` `instMul`	—	—
`mk_sub_mk` 📖	mathematical	—	`QuadraticAlgebra` `instSub`	—	—
`mul_C_eq_smul` 📖	mathematical	—	`QuadraticAlgebra` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toAdd` `C` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instSMul` `Algebra.toSMul` `Algebra.id`	—	`mul_comm` `C_mul_eq_smul`
`mul_coe_eq_smul` 📖	mathematical	—	`QuadraticAlgebra` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toAdd` `C` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instSMul` `Algebra.toSMul` `Algebra.id`	—	`mul_C_eq_smul`
`neg_mk` 📖	mathematical	—	`QuadraticAlgebra` `instNeg`	—	—
`nsmul_mk` 📖	mathematical	—	`QuadraticAlgebra` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`ext` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `add_zero`
`rank_eq_two` 📖	mathematical	—	`Module.rank` `QuadraticAlgebra` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instModule` `Semiring.toModule` `Cardinal` `instOfNatAtLeastTwo` `Cardinal.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `rank_eq_card_basis` `Fintype.card_fin`
`re_C` 📖	mathematical	—	`re` `C`	—	—
`re_add` 📖	mathematical	—	`re` `QuadraticAlgebra` `instAdd`	—	—
`re_coe` 📖	mathematical	—	`re` `C`	—	`re_C`
`re_intCast` 📖	mathematical	—	`re` `QuadraticAlgebra` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `instAddCommGroupWithOne`	—	—
`re_mul` 📖	mathematical	—	`re` `QuadraticAlgebra` `instMul` `im`	—	—
`re_natCast` 📖	mathematical	—	`re` `QuadraticAlgebra` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	—	—
`re_neg` 📖	mathematical	—	`re` `QuadraticAlgebra` `instNeg`	—	—
`re_ofNat` 📖	mathematical	—	`re`	—	—
`re_one` 📖	mathematical	—	`re` `QuadraticAlgebra` `instOne`	—	—
`re_smul` 📖	mathematical	—	`re` `QuadraticAlgebra` `instSMul`	—	—
`re_sub` 📖	mathematical	—	`re` `QuadraticAlgebra` `instSub`	—	—
`re_zero` 📖	mathematical	—	`re` `QuadraticAlgebra` `instZero`	—	—
`reₗ_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `QuadraticAlgebra` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `reₗ` `re`	—	—
`smul_C` 📖	mathematical	—	`QuadraticAlgebra` `instSMul` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `C` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`C_mul` `C_mul_eq_smul`
`smul_coe` 📖	mathematical	—	`QuadraticAlgebra` `instSMul` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `C` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`smul_C`
`smul_mk` 📖	mathematical	—	`QuadraticAlgebra` `instSMul`	—	—
`zsmul_val` 📖	mathematical	—	`QuadraticAlgebra` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing`	—	`ext` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `add_zero`

(root)

Definitions

Name	Category	Theorems
`instDecidableEqQuadraticAlgebra` 📖	CompOp	—

instDecidableEqQuadraticAlgebra

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

---

← Back to Index