Discriminant

📁 Source: Mathlib/RingTheory/Discriminant.lean

Statistics

Metric	Count
Definitions discr	1
Theorems discr_def, discr_eq_det_embeddingsMatrixReindex_pow_two, discr_eq_discr, discr_eq_discr_of_algEquiv, discr_isIntegral, discr_isUnit_of_basis, discr_mul_isIntegral_mem_adjoin, discr_not_zero_of_basis, discr_of_matrix_mulVec, discr_of_matrix_vecMul, discr_powerBasis_eq_norm, discr_powerBasis_eq_prod, discr_powerBasis_eq_prod', discr_powerBasis_eq_prod'', discr_reindex, discr_zero_of_not_linearIndependent	16
Total	17

Algebra

Definitions

Name	Category	Theorems
discr 📖	CompOp	30 math math: IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow, IsCyclotomicExtension.discr_odd_prime, discr_eq_discr, IsCyclotomicExtension.Rat.discr_prime_pow', discr_powerBasis_eq_norm, discr_eq_discr_of_toMatrix_coeff_isIntegral, discr_eq_discr_of_algEquiv, IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one, NumberField.discr_eq_discr, IsCyclotomicExtension.Rat.discr_prime_pow_ne_two', discr_of_matrix_mulVec, IsCyclotomicExtension.discr_prime_pow_ne_two, discr_of_matrix_vecMul, discr_mul_isIntegral_mem_adjoin, isIntegral_discr_mul_of_mem_traceDual, discr_powerBasis_eq_prod, discr_def, discr_isUnit_of_basis, discr_eq_det_embeddingsMatrixReindex_pow_two, discr_localizationLocalization, discr_powerBasis_eq_prod'', discr_powerBasis_eq_prod', IsCyclotomicExtension.Rat.discr_odd_prime', NumberField.coe_discr, discr_zero_of_not_linearIndependent, discr_isIntegral, IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow', IsCyclotomicExtension.discr_prime_pow, IsCyclotomicExtension.discr_prime_pow_ne_two', discr_reindex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discr_def 📖	mathematical	—	discr Matrix.det traceMatrix	—	—
discr_eq_det_embeddingsMatrixReindex_pow_two 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap discr EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.det embeddingsMatrixReindex	—	discr_def RingHom.map_det RingHom.mapMatrix_apply traceMatrix_eq_embeddingsMatrixReindex_mul_trans Matrix.det_mul Matrix.det_transpose pow_two
discr_eq_discr 📖	mathematical	—	discr Int.instCommRing Ring.toIntAlgebra CommRing.toRing DFunLike.coe Module.Basis Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toIntModule Ring.toAddCommGroup Module.Basis.instFunLike	—	Module.Basis.toMatrix_map_vecMul RingHomInvPair.ids smulCommClass_self Finite.of_fintype LinearMap.toMatrix_id_eq_basis_toMatrix LinearEquiv.isUnit_det sq_eq_one_iff IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE Int.isUnit_iff one_mul discr_of_matrix_vecMul
discr_eq_discr_of_algEquiv 📖	mathematical	—	discr DFunLike.coe AlgEquiv CommRing.toCommSemiring CommSemiring.toSemiring AlgEquiv.instFunLike	—	discr_def Matrix.ext map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass trace_eq_of_algEquiv
discr_isIntegral 📖	mathematical	IsIntegral DivisionRing.toRing Field.toDivisionRing	discr EuclideanDomain.toCommRing Field.toEuclideanDomain	—	discr_def IsIntegral.det isIntegral_trace IsIntegral.mul
discr_isUnit_of_basis 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield discr EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe Module.Basis NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule Semifield.toCommSemiring Module.Basis.instFunLike	—	discr_not_zero_of_basis
discr_mul_isIntegral_mem_adjoin 📖	mathematical	IsIntegral DivisionRing.toRing Field.toDivisionRing PowerBasis.gen EuclideanDomain.toCommRing Field.toEuclideanDomain	Subalgebra CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SetLike.instMembership Subalgebra.instSetLike adjoin Set Set.instSingletonSet toSMul Semifield.toCommSemiring discr PowerBasis.dim Fin.fintype DFunLike.coe Module.Basis CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing toModule Ring.toSemiring Module.Basis.instFunLike PowerBasis.basis	—	Matrix.det.congr_simp PowerBasis.coe_basis discr.congr_simp discr_isUnit_of_basis RingHomInvPair.ids Finite.of_fintype traceMatrix_of_basis_mulVec Matrix.mulVec_cramer Matrix.mulVec_smul to_smulCommClass Matrix.one_mulVec Matrix.nonsing_inv_mul Matrix.mulVec_mulVec Matrix.cramer_apply Matrix.det_apply Subalgebra.sum_mem Subalgebra.zsmul_mem Subalgebra.prod_mem Matrix.updateCol.congr_simp Matrix.updateCol_apply mem_bot IsIntegrallyClosed.isIntegral_iff isIntegral_trace IsIntegral.mul IsIntegral.pow Module.Basis.sum_repr Finset.smul_sum Pi.smul_apply discr_def smul_assoc IsScalarTower.left Module.Basis.equivFun_apply algebraMap_smul Subalgebra.smul_mem PowerBasis.basis_eq_pow Subalgebra.pow_mem subset_adjoin Set.mem_singleton
discr_not_zero_of_basis 📖	—	—	—	—	discr_def RingHomInvPair.ids to_smulCommClass LinearMap.instSMulCommClass traceMatrix_of_basis LinearMap.BilinForm.nondegenerate_iff_det_ne_zero instIsDomain traceForm_nondegenerate
discr_of_matrix_mulVec 📖	mathematical	—	discr Matrix.mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.det	—	discr_def traceMatrix_of_matrix_mulVec Matrix.det_mul Matrix.det_transpose mul_comm mul_assoc pow_two
discr_of_matrix_vecMul 📖	mathematical	—	discr Matrix.vecMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.det	—	discr_def traceMatrix_of_matrix_vecMul Matrix.det_mul Matrix.det_transpose mul_comm mul_assoc pow_two
discr_powerBasis_eq_norm 📖	mathematical	—	discr PowerBasis.dim EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing Fin.fintype DFunLike.coe Module.Basis CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing toModule Ring.toSemiring Module.Basis.instFunLike PowerBasis.basis Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Module.finrank Semifield.toCommSemiring MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidHom.instFunLike norm AlgHom Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra id AlgHom.funLike Polynomial.aeval PowerBasis.gen LinearMap RingHom.id NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative minpoly	—	instIsDomain Fintype.card_fin AlgHom.card AlgebraicClosure.isAlgClosed PowerBasis.finrank commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.nodup_roots Polynomial.Separable.map IsSeparable.isSeparable Polynomial.mem_roots DivisionRing.isSimpleRing minpoly.ne_zero PowerBasis.isIntegral_gen Polynomial.IsRoot.def Polynomial.eval_map_algebraMap Polynomial.aeval_algHom_apply AlgHom.algHomClass minpoly.aeval map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass RingHom.injective map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass map_neg RingHomClass.toAddMonoidHomClass map_one MonoidHomClass.toOneHomClass discr_powerBasis_eq_prod'' norm_eq_prod_embeddings Finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag Multiset.Nodup.erase Polynomial.derivative_map Polynomial.Splits.eval_root_derivative IsAlgClosed.splits Polynomial.Monic.map minpoly.monic Finset.prod_sigma' Finset.prod_bij' Polynomial.eval₂_eq_eval_map Multiset.Nodup.mem_erase_iff Equiv.injective PowerBasis.algHom_ext Equiv.apply_symm_apply PowerBasis.lift_gen Equiv.symm_apply_apply
discr_powerBasis_eq_prod 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap discr PowerBasis.dim EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing Fin.fintype Module.Basis CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing toModule Ring.toSemiring Module.Basis.instFunLike PowerBasis.basis Finset.prod CommRing.toCommMonoid Finset.univ Finset.Ioi PartialOrder.toPreorder Fin.instPartialOrder Fin.instLocallyFiniteOrderTop Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AlgHom AlgHom.funLike Equiv EquivLike.toFunLike Equiv.instEquivLike PowerBasis.gen	—	discr_eq_det_embeddingsMatrixReindex_pow_two embeddingsMatrixReindex_eq_vandermonde Matrix.det_transpose Matrix.det_vandermonde Finset.prod_pow
discr_powerBasis_eq_prod' 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap discr PowerBasis.dim EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing Fin.fintype Module.Basis CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing toModule Ring.toSemiring Module.Basis.instFunLike PowerBasis.basis Finset.prod CommRing.toCommMonoid Finset.univ Finset.Ioi PartialOrder.toPreorder Fin.instPartialOrder Fin.instLocallyFiniteOrderTop NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AlgHom AlgHom.funLike Equiv EquivLike.toFunLike Equiv.instEquivLike PowerBasis.gen	—	discr_powerBasis_eq_prod Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr
discr_powerBasis_eq_prod'' 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap discr PowerBasis.dim EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing Fin.fintype Module.Basis CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing toModule Ring.toSemiring Module.Basis.instFunLike PowerBasis.basis Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Module.finrank Finset.prod CommRing.toCommMonoid Finset.univ Finset.Ioi PartialOrder.toPreorder Fin.instPartialOrder Fin.instLocallyFiniteOrderTop SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup AlgHom AlgHom.funLike Equiv EquivLike.toFunLike Equiv.instEquivLike PowerBasis.gen	—	discr_powerBasis_eq_prod' Finset.prod_congr neg_eq_neg_one_mul Finset.prod_mul_distrib Finset.prod_const Finset.prod_pow_eq_pow_sum Rat.instCharZero Nat.cast_sum Nat.instNoMaxOrder Finset.sum_congr Fin.card_Ioi add_comm Nat.cast_sub Nat.cast_add Nat.cast_one Finset.sum_sub_distrib Finset.sum_const Finset.card_fin nsmul_eq_mul Finset.sum_add_distrib mul_one Finset.sum_range Finset.sum_range_id instIsDomain AlgHom.card Fintype.card_fin Fintype.card_congr Even.two_dvd Nat.even_mul_pred_self Nat.instAtLeastTwoHAddOfNat zero_lt_iff Module.finrank_pos_iff commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Nat.cast_div Nat.cast_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.neg_mul
discr_reindex 📖	mathematical	—	discr DFunLike.coe Module.Basis CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule Module.Basis.instFunLike Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	Module.Basis.coe_reindex discr_def traceMatrix_reindex Matrix.det_reindex_self
discr_zero_of_not_linearIndependent 📖	mathematical	LinearIndependent CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule	discr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Fintype.not_linearIndependent_iff mul_comm mul_smul_comm map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass MulZeroClass.zero_mul map_zero AddMonoidHomClass.toZeroHomClass Matrix.eq_zero_of_mulVec_eq_zero discr_def

---

← Back to Index