Documentation Verification Report

EquivReindex

📁 Source: Mathlib/NumberTheory/NumberField/EquivReindex.lean

Statistics

Metric	Count
Definitions `basisMatrix`, `equivReindex`, `instInvertibleMatrixRingHomComplexBasisMatrix`	3
Theorems `basisMatrix_eq_embeddingsMatrixReindex`, `canonicalEmbedding_eq_basisMatrix_mulVec`, `conj_basisMatrix`, `det_of_basisMatrix_non_zero`, `inverse_basisMatrix_mulVec_eq_repr`	5
Total	8

NumberField

Definitions

Name	Category	Theorems
`basisMatrix` 📖	CompOp	5 math math: `basisMatrix_eq_embeddingsMatrixReindex`, `discr_eq_basisMatrix_det_sq`, `conj_basisMatrix`, `inverse_basisMatrix_mulVec_eq_repr`, `canonicalEmbedding_eq_basisMatrix_mulVec`
`equivReindex` 📖	CompOp	4 math math: `basisMatrix_eq_embeddingsMatrixReindex`, `inverse_basisMatrix_mulVec_eq_repr`, `canonicalEmbedding_eq_basisMatrix_mulVec`, `house.basis_repr_norm_le_const_mul_house`
`instInvertibleMatrixRingHomComplexBasisMatrix` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basisMatrix_eq_embeddingsMatrixReindex` 📖	mathematical	—	`basisMatrix` `Algebra.embeddingsMatrixReindex` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring` `Rat.commRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `to_charZero` `Complex.commRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `Complex.instNormedField` `Complex.instCharZero` `Module.Free.ChooseBasisIndex` `RingOfIntegers` `Int.instSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `RingOfIntegers.instCommRing` `AddCommGroup.toIntModule` `Ring.toAddCommGroup` `CommRing.toRing` `RingOfIntegers.instFreeInt` `DFunLike.coe` `Module.Basis` `Rat.semiring` `Algebra.toModule` `Rat.commSemiring` `Module.Basis.instFunLike` `integralBasis` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivReindex` `RingHom.equivRatAlgHom` `DivisionRing.toRing` `Complex.instRing`	—	`Matrix.ext` `to_charZero` `Complex.instCharZero` `RingOfIntegers.instFreeInt` `canonicalEmbedding.latticeBasis_apply` `integralBasis_apply`
`canonicalEmbedding_eq_basisMatrix_mulVec` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Pi.nonAssocSemiring` `Complex` `Complex.instSemiring` `RingHom.instFunLike` `canonicalEmbedding` `Matrix.mulVec` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Embeddings.instFintypeRingHom` `Complex.instField` `Complex.instCharZero` `Matrix.transpose` `basisMatrix` `Complex.instRatCast` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Rat.semiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `NonUnitalNonAssocSemiring.toAddCommMonoid` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finsupp.instAddCommMonoid` `Algebra.toModule` `Rat.commSemiring` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `to_charZero` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `Module.Basis.reindex` `Module.Free.ChooseBasisIndex` `RingOfIntegers` `Int.instSemiring` `RingOfIntegers.instCommRing` `AddCommGroup.toIntModule` `Ring.toAddCommGroup` `CommRing.toRing` `RingOfIntegers.instFreeInt` `integralBasis` `Equiv.symm` `equivReindex`	—	`Complex.instCharZero` `RingHomInvPair.ids` `to_charZero` `RingOfIntegers.instFreeInt` `Module.IsNoetherian.finite` `RingOfIntegers.instIsNoetherianInt` `Module.Basis.sum_repr` `Equiv.sum_comp` `Finset.sum_congr` `canonicalEmbedding.integralBasis_repr_apply` `Fintype.sum_apply` `Module.Basis.repr_reindex` `Finsupp.mapDomain_equiv_apply` `mul_comm`
`conj_basisMatrix` 📖	mathematical	—	`Matrix.map` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring` `basisMatrix` `DFunLike.coe` `CommSemiring.toSemiring` `Complex.instCommSemiring` `RingHom.instFunLike` `starRingEnd` `Complex.instStarRing` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.reindex` `Equiv.refl` `Function.Involutive.toPerm` `ComplexEmbedding.conjugate` `ComplexEmbedding.involutive_conjugate`	—	`Matrix.ext` `ComplexEmbedding.involutive_conjugate` `RingOfIntegers.instFreeInt` `to_charZero` `canonicalEmbedding.latticeBasis_apply` `integralBasis_apply`
`det_of_basisMatrix_non_zero` 📖	—	—	—	—	`Complex.instCharZero` `to_charZero` `RingOfIntegers.instFreeInt` `basisMatrix_eq_embeddingsMatrixReindex` `pow_ne_zero_iff` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `two_ne_zero` `Module.IsNoetherian.finite` `RingOfIntegers.instIsNoetherianInt` `Algebra.discr_reindex` `Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two` `to_finiteDimensional` `Complex.isAlgClosed` `Algebra.IsAlgebraic.isSeparable_of_perfectField` `Algebra.IsAlgebraic.of_finite` `Rat.nontrivial` `PerfectField.ofCharZero` `Rat.instCharZero` `map_ne_zero_iff` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `RingHom.injective` `DivisionRing.isSimpleRing` `Complex.instNontrivial` `Algebra.discr_not_zero_of_basis`
`inverse_basisMatrix_mulVec_eq_repr` 📖	mathematical	—	`Matrix.mulVec` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Embeddings.instFintypeRingHom` `Complex.instField` `Complex.instCharZero` `Matrix` `Matrix.inv` `Complex.commRing` `Matrix.transpose` `basisMatrix` `DFunLike.coe` `Pi.nonAssocSemiring` `RingHom.instFunLike` `canonicalEmbedding` `RingOfIntegers` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingOfIntegers.instCommRing` `algebraMap` `RingOfIntegers.instAlgebra_1` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.id` `Semifield.toCommSemiring` `Complex.instRatCast` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Rat.semiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `NonUnitalNonAssocSemiring.toAddCommMonoid` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finsupp.instAddCommMonoid` `Algebra.toModule` `Rat.commSemiring` `DivisionRing.toRatAlgebra` `to_charZero` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `Module.Basis.reindex` `Module.Free.ChooseBasisIndex` `Int.instSemiring` `AddCommGroup.toIntModule` `Ring.toAddCommGroup` `CommRing.toRing` `RingOfIntegers.instFreeInt` `integralBasis` `Equiv.symm` `equivReindex` `RingOfIntegers.val`	—	`Complex.instCharZero` `RingHomInvPair.ids` `to_charZero` `RingOfIntegers.instFreeInt` `Matrix.inv_mulVec_eq_vec` `canonicalEmbedding_eq_basisMatrix_mulVec`

---

← Back to Index