Determinant

📁 Source: Mathlib/LinearAlgebra/Determinant.lean

Statistics

Metric	Count
Definitions det, ofIsUnitDet, det, detAux, equivOfDetNeZero, equivOfIsUnitDet, indexEquivOfInv, det, equivOfPiLEquivPi	9
Theorems eq_smul_basis_det, map_basis_eq_zero_iff, map_basis_ne_zero_iff, coe_det, coe_inv_det, coe_ofIsUnitDet, det_coe_symm, det_conj, det_mul_det_symm, det_refl, det_symm, det_symm_mul_det, det_trans, isUnit_det, isUnit_det', ofIsUnitDet_apply, ofIsUnitDet_symm_apply, associated_det_comp_equiv, associated_det_of_eq_comp, bot_lt_ker_of_det_eq_zero, coe_det, coe_equivOfIsUnitDet, detAux_comp, detAux_def, detAux_def', detAux_def'', detAux_id, det_cases, det_comp, det_conj, det_def, det_dualMap, det_eq_det_mul_det, det_eq_det_toMatrix_of_finset, det_eq_one_of_finrank_eq_zero, det_eq_one_of_not_module_finite, det_eq_one_of_subsingleton, det_eq_zero_iff_ker_ne_bot, det_id, det_map, det_mulLeft, det_mulRight, det_pi, det_prodMap, det_ring, det_smul, det_toLin, det_toLin', det_toMatrix, det_toMatrix', det_toMatrix_eq_det_toMatrix, det_zero, det_zero', equivOfIsUnitDet_apply, finiteDimensional_of_det_ne_one, finite_of_det_ne_one, free_of_det_ne_one, isUnit_det, isUnit_iff_isUnit_det, range_lt_top_of_det_eq_zero, det_comm, det_comm', det_conj_of_mul_eq_one, det_map, det_apply, det_basis, det_comp, det_comp_basis, det_inv, det_isEmpty, det_isUnitSMul, det_map, det_map', det_mul_det, det_ne_zero, det_reindex, det_reindex', det_reindex_symm, det_self, det_smul_mk_coord_eq_det_update, det_unitsSMul, det_unitsSMul_self, isUnit_det, is_basis_iff_det, smul_det, of_det_ne_one, basisFun_det, basisFun_det_apply	88
Total	97

AlternatingMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_smul_basis_det 📖	mathematical	—	AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule instSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id DFunLike.coe instFunLike Module.Basis Module.Basis.instFunLike Module.Basis.det	—	Module.Basis.ext_alternating Finite.of_fintype Algebra.to_smulCommClass Finite.injective_iff_bijective map_perm Module.Basis.det_self mul_one
map_basis_eq_zero_iff 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule instFunLike Module.Basis Module.Basis.instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass instZero	—	nonempty_fintype Algebra.to_smulCommClass zero_smul eq_smul_basis_det zero_apply
map_basis_ne_zero_iff 📖	—	—	—	—	map_basis_eq_zero_iff

LinearEquiv

Definitions

Name	Category	Theorems
det 📖	CompOp	37 math math: Complex.linearEquiv_det_conjLIE, Orientation.linearEquiv_det_rotation, transvection.det_eq_one, det_trans, ZLattice.covolume_eq_det_inv, SpecialLinearGroup.coe_zpow, SpecialLinearGroup.toLinearEquiv_symm_to_linearMap, SpecialLinearGroup.mem_center_iff_spec, SpecialLinearGroup.mem_center_iff, SpecialLinearGroup.coe_one, SpecialLinearGroup.mem_range_toGeneralLinearGroup_iff, det_baseChange, SpecialLinearGroup.coe_inv, SpecialLinearGroup.congr_linearEquiv_coe_apply, SpecialLinearGroup.det_eq_one, Submodule.linearEquiv_det_reflection, Orientation.map_eq_det_inv_smul, det_symm, SpecialLinearGroup.centerEquivRootsOfUnity_symm_apply, SpecialLinearGroup.det_coe, SpecialLinearGroup.coe_mul, det_conj, SpecialLinearGroup.coe_pow, Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, Complex.linearEquiv_det_conjAe, SpecialLinearGroup.centerEquivRootsOfUnity_apply, linearEquiv_det_rotation, Module.Basis.map_orientation_eq_det_inv_smul, Polynomial.det_taylorLinearEquiv, Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq, coe_inv_det, det_refl, SpecialLinearGroup.baseChange_apply_coe, SpecialLinearGroup.coe_div, SpecialLinearGroup.coe_dualMap, SpecialLinearGroup.toLinearEquiv_to_linearMap, coe_det
ofIsUnitDet 📖	CompOp	3 math math: coe_ofIsUnitDet, ofIsUnitDet_apply, ofIsUnitDet_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_det 📖	mathematical	—	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Units MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid automorphismGroup Units.instMulOneClass MonoidHom.instFunLike det LinearMap MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring LinearMap.det toLinearMap	—	RingHomInvPair.ids
coe_inv_det 📖	mathematical	—	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units Units.instInv DFunLike.coe MonoidHom LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid automorphismGroup Units.instMulOneClass MonoidHom.instFunLike det LinearMap MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring LinearMap.det toLinearMap symm	—	RingHomInvPair.ids
coe_ofIsUnitDet 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Matrix.det DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap AddCommGroup.toAddCommMonoid Matrix LinearMap.addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix Finite.of_fintype	toLinearMap ofIsUnitDet	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype LinearMap.ext
det_coe_symm 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHomInvPair.ids symm InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	RingHomInvPair.ids Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg IsUnit.ne_zero EuclideanDomain.toNontrivial isUnit_det' Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial det_symm_mul_det
det_conj 📖	mathematical	—	DFunLike.coe MonoidHom LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid automorphismGroup Units.instMulOneClass MonoidHom.instFunLike det trans RingHomCompTriple.ids symm	—	RingHomInvPair.ids RingHomCompTriple.ids coe_det comp_coe LinearMap.det_conj
det_mul_det_symm 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det toLinearMap RingHomInvPair.ids symm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	RingHomInvPair.ids RingHomCompTriple.ids symm_trans_self LinearMap.det_id
det_refl 📖	mathematical	—	DFunLike.coe MonoidHom LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid automorphismGroup Units.instMulOneClass MonoidHom.instFunLike det refl Units.instOne	—	Units.ext RingHomInvPair.ids LinearMap.det_id
det_symm 📖	mathematical	—	DFunLike.coe MonoidHom LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid automorphismGroup Units.instMulOneClass MonoidHom.instFunLike det symm InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	RingHomInvPair.ids map_inv MonoidHom.instMonoidHomClass
det_symm_mul_det 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det toLinearMap RingHomInvPair.ids symm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	RingHomInvPair.ids RingHomCompTriple.ids self_trans_symm LinearMap.det_id
det_trans 📖	mathematical	—	DFunLike.coe MonoidHom LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid automorphismGroup Units.instMulOneClass MonoidHom.instFunLike det trans RingHomCompTriple.ids Units.instMul	—	RingHomInvPair.ids map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass
isUnit_det 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Matrix.det DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap AddCommGroup.toAddCommMonoid Matrix LinearMap.addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix Finite.of_fintype toLinearMap	—	RingHomInvPair.ids Matrix.isUnit_det_of_left_inverse smulCommClass_self Finite.of_fintype RingHomCompTriple.ids self_trans_symm LinearMap.toMatrix_id_eq_basis_toMatrix Module.Basis.toMatrix_self LinearMap.toMatrix_comp
isUnit_det' 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det toLinearMap RingHomInvPair.ids	—	RingHomInvPair.ids IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid det_mul_det_symm
ofIsUnitDet_apply 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Matrix.det DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap AddCommGroup.toAddCommMonoid Matrix LinearMap.addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix Finite.of_fintype	instEquivLike ofIsUnitDet LinearMap.instFunLike	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype
ofIsUnitDet_symm_apply 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Matrix.det DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap AddCommGroup.toAddCommMonoid Matrix LinearMap.addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix Finite.of_fintype	instEquivLike symm ofIsUnitDet LinearMap.instFunLike Matrix.toLin Matrix.inv	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype

LinearMap

Definitions

Name	Category	Theorems
det 📖	CompOp	76 math math: det_toContinuousLinearMap, Module.Basis.det_comp_basis, MeasureTheory.Measure.addHaar_image_continuousLinearMap, det_mulLeft, det_pi, det_zero, Orientation.map_eq_neg_iff_det_neg, det_baseChange, isUnit_iff_isUnit_det, det_mulRight, Orientation.det_rotation, associated_det_of_eq_comp, Orientation.map_eq_iff_det_pos, det_def, det_eq_one_of_not_module_finite, MeasureTheory.Measure.map_linearMap_addHaar_eq_smul_addHaar, IsBaseChange.det_endHom, MeasureTheory.Measure.addHaar_preimage_continuousLinearMap, LinearEquiv.det_symm_mul_det, det_prodMap, SpecialLinearGroup.det_eq_one, det_eq_det_toMatrix_of_finset, det_toLin', Complex.det_conjAe, Algebra.PreSubmersivePresentation.jacobian_eq_det_aevalDifferential, Polynomial.det_taylorLinearEquiv_toLinearMap, isUnit_det, det_eq_zero_iff_ker_ne_bot, Submodule.natAbs_det_equiv, LinearEquiv.isUnit_det', Module.Basis.orientation_comp_linearEquiv_eq_iff_det_pos, Module.Basis.orientation_comp_linearEquiv_eq_neg_iff_det_neg, det_map, hasEigenvalue_zero_tfae, MeasureTheory.Measure.addHaar_image_linearMap, eval_charpoly, det_dualMap, det_id, Submodule.det_reflection, Module.Basis.det_comp, det_restrictScalars, MeasureTheory.Measure.addHaar_image_continuousLinearEquiv, det_eq_sign_charpoly_coeff, Real.map_linearMap_volume_pi_eq_smul_volume_pi, MeasureTheory.Measure.map_linearMap_addHaar_pi_eq_smul_addHaar, det_eq_one_of_finrank_eq_zero, Module.Basis.det_basis, det_smul, MeasureTheory.Measure.addHaar_preimage_linearMap, Ideal.natAbs_det_equiv, MeasureTheory.Measure.addHaar_preimage_continuousLinearEquiv, det_comp, transvection.det, LinearEquiv.det_mul_det_symm, Algebra.norm_apply, Algebra.norm_eq_zero_iff', det_conj, det_zero'', MeasureTheory.Measure.addHaar_preimage_linearEquiv, det_zero', LinearEquiv.coe_inv_det, det_rotation, det_ring, coe_det, det_eq_det_mul_det, LinearEquiv.det_coe_symm, det_toMatrix', det_cases, not_hasEigenvalue_zero_tfae, QuadraticAlgebra.det_toLinearMap_eq_norm, det_toMatrix, det_toLin, det_eq_one_of_subsingleton, associated_det_comp_equiv, Complex.det_conjLIE, LinearEquiv.coe_det
detAux 📖	CompOp	7 math math: detAux_def'', det_def, detAux_def, detAux_def', detAux_comp, coe_det, detAux_id
equivOfDetNeZero 📖	CompOp	—
equivOfIsUnitDet 📖	CompOp	2 math math: coe_equivOfIsUnitDet, equivOfIsUnitDet_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associated_det_comp_equiv 📖	mathematical	—	Associated MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det comp RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids	—	RingHomInvPair.ids associated_det_of_eq_comp RingHomCompTriple.ids LinearEquiv.apply_symm_apply
associated_det_of_eq_comp 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instFunLike LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv	Associated MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det	—	RingHomInvPair.ids RingHomCompTriple.ids mul_one det_comp Associated.mul_left associated_one_iff_isUnit LinearEquiv.isUnit_det' ext
bot_lt_ker_of_det_eq_zero 📖	mathematical	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Submodule Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder Bot.bot Submodule.instBot ker	—	finite_of_det_ne_one NeZero.one IsDomain.toNontrivial commRing_strongRankCondition RingHomInvPair.ids smulCommClass_self Finite.of_fintype Matrix.exists_mulVec_eq_zero_iff det_toMatrix LinearEquiv.injective Module.Basis.equivFun_symm_apply map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass Finset.sum_congr map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_zero AddMonoidHomClass.toZeroHomClass Finset.sum_apply toMatrix_apply mul_comm LinearEquiv.map_ne_zero_iff
coe_det 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det Finset Module.Basis SetLike.instMembership Finset.instSetLike detAux Finset.Subtype.fintype Nonempty.some instOneMonoidHom	—	det_def
coe_equivOfIsUnitDet 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det	LinearEquiv.toLinearMap RingHomInvPair.ids equivOfIsUnitDet	—	ext RingHomInvPair.ids equivOfIsUnitDet_apply
detAux_comp 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike detAux comp RingHomCompTriple.ids Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	MonoidHom.map_mul
detAux_def 📖	mathematical	—	detAux Trunc.lift Module.Basis CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid MonoidHom LinearMap RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.comp Matrix Matrix.instMulOneOfFintypeOfDecidableEqOfAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.detMonoidHom MonoidHomClass.toMonoidHom AlgEquiv Matrix.semiring Module.End.instAlgebra Algebra.toSMul Algebra.id Matrix.instAlgebra AlgEquiv.instFunLike toMatrixAlgEquiv	—	—
detAux_def' 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike detAux Module.Basis Matrix.det LinearEquiv RingHomInvPair.ids Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finite.of_fintype	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype detAux_def
detAux_def'' 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike detAux Matrix.det LinearEquiv RingHomInvPair.ids Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finite.of_fintype	—	Trunc.induction_on RingHomInvPair.ids smulCommClass_self Finite.of_fintype detAux_def' det_toMatrix_eq_det_toMatrix
detAux_id 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike detAux id AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	MonoidHom.map_one
det_cases 📖	mathematical	Matrix.det Finset SetLike.instMembership Finset.instSetLike Finset.Subtype.fintype DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap AddCommGroup.toAddCommMonoid Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finite.of_fintype AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype det_toMatrix det_def
det_comp 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det comp RingHomCompTriple.ids Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	MonoidHom.map_mul
det_conj 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det comp RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm	—	RingHomInvPair.ids RingHomCompTriple.ids smulCommClass_self Finite.of_fintype det_toMatrix toMatrix_comp Matrix.mul_assoc Matrix.det_conj_of_mul_eq_one LinearEquiv.comp_coe RingHomInvPair.triples₂ LinearEquiv.symm_trans_self LinearEquiv.refl_toLinearMap toMatrix_id LinearEquiv.self_trans_symm Mathlib.Tactic.Contrapose.contrapose₄ coe_det
det_def 📖	mathematical	—	det MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Finset Module.Basis SetLike.instMembership Finset.instSetLike detAux Finset.Subtype.fintype Nonempty.some instOneMonoidHom	—	—
det_dualMap 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual AddCommGroup.toAddCommMonoid addCommGroup Ring.toAddCommGroup CommRing.toRing Semiring.toModule module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det dualMap	—	smulCommClass_self RingHomInvPair.ids Finite.of_fintype det_toMatrix Matrix.det.congr_simp toMatrix_transpose Matrix.det_transpose
det_eq_det_mul_det 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.comap RingHom.id Semiring.toNonAssocSemiring	DFunLike.coe MonoidHom LinearMap MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SetLike.instMembership Submodule.setLike Submodule.addCommGroup CommRing.toRing Submodule.module restrict HasQuotient.Quotient Ring.toSemiring Submodule.hasQuotient Submodule.Quotient.addCommGroup Submodule.Quotient.module Submodule.mapQ	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype Module.Finite.quotient Finite.instSum Matrix.ext toMatrix_apply Module.Basis.sumQuot_inl Module.Basis.sumQuot_repr_inl_of_mem mem_ker Submodule.ker_mkQ Submodule.coe_mem Module.Basis.sumQuot_repr_inr map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Module.Basis.sumQuot_inr Submodule.mapQ_apply det_toMatrix Matrix.det_fromBlocks_zero₂₁
det_eq_det_toMatrix_of_finset 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det Matrix.det Finset SetLike.instMembership Finset.instSetLike Finset.Subtype.fintype LinearEquiv RingHomInvPair.ids Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finite.of_fintype	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype coe_det detAux_def''
det_eq_one_of_finrank_eq_zero 📖	mathematical	Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	det_cases Fintype.card_eq_zero_iff Module.finrank_eq_card_basis commRing_strongRankCondition EuclideanDomain.toNontrivial Matrix.det_isEmpty RingHomInvPair.ids smulCommClass_self Finite.of_fintype
det_eq_one_of_not_module_finite 📖	mathematical	Module.Finite CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	DFunLike.coe MonoidHom LinearMap RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	det_def Module.Finite.of_basis Finite.of_fintype MonoidHom.one_apply
det_eq_one_of_subsingleton 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Fin.isEmpty' RingHomInvPair.ids smulCommClass_self Finite.of_fintype det_toMatrix Matrix.det_isEmpty
det_eq_zero_iff_ker_ne_bot 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	bot_lt_iff_ne_bot bot_lt_ker_of_det_eq_zero commRing_strongRankCondition IsDomain.toNontrivial Submodule.ne_bot_iff RingHomInvPair.ids smulCommClass_self Finite.of_fintype det_toMatrix Matrix.exists_mulVec_eq_zero_iff EquivLike.toEmbeddingLike AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass toMatrix_mulVec_repr
det_id 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det id AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	MonoidHom.map_one
det_map 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det Module.End DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield EquivLike.toFunLike	—	smulCommClass_self IsScalarTower.left RingHomInvPair.ids AlgEquiv.eq_linearEquivConjAlgEquiv Module.Projective.of_free Module.Free.of_divisionRing det_conj
det_mulLeft 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Ring.toAddCommGroup CommRing.toRing Semiring.toModule MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det mulLeft NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.to_smulCommClass Algebra.id	—	Algebra.to_smulCommClass det_ring mul_one
det_mulRight 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Ring.toAddCommGroup CommRing.toRing Semiring.toModule MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det mulRight NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsScalarTower.right Algebra.id	—	IsScalarTower.right det_ring one_mul
det_pi 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Pi.addCommGroup Pi.module MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det pi Pi.addCommMonoid comp RingHomCompTriple.ids proj Finset.prod CommRing.toCommMonoid Finset.univ	—	RingHomCompTriple.ids RingHomInvPair.ids smulCommClass_self Finite.of_fintype det_toMatrix Finset.prod_congr Finite.instProd Matrix.ext toMatrix_apply' Module.Basis.coe_reindex Module.Basis.repr_reindex_apply Pi.basis_apply Pi.single_apply map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Matrix.det_blockDiagonal
det_prodMap 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Prod.instAddCommGroup Prod.instModule MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det prodMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype det_toMatrix Finite.instSum toMatrix_prodMap Matrix.det_fromBlocks_zero₂₁
det_ring 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Ring.toAddCommGroup CommRing.toRing Semiring.toModule MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instFunLike AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype det_toMatrix Matrix.det_unique toMatrix_singleton
det_smul 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow Module.finrank	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim smulCommClass_self Module.finrank_subsingleton pow_one Module.Finite.of_basis Finite.of_fintype RingHomInvPair.ids commRing_strongRankCondition det_toMatrix Matrix.det.congr_simp map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Matrix.det_smul Fintype.card_fin finrank_eq_zero_of_not_exists_basis coe_det pow_zero mul_one
det_toLin 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det LinearEquiv RingHomInvPair.ids Matrix Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring addCommMonoid Matrix.module Semiring.toModule module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLin Finite.of_fintype Matrix.det	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype det_toMatrix toMatrix_toLin
det_toLin' 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Pi.addCommGroup Ring.toAddCommGroup CommRing.toRing Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det LinearEquiv RingHomInvPair.ids Matrix Pi.addCommMonoid Matrix.addCommMonoid addCommMonoid Matrix.module module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLin' Matrix.det	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass det_toLin Finite.of_fintype
det_toMatrix 📖	mathematical	—	Matrix.det DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap AddCommGroup.toAddCommMonoid Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finite.of_fintype MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype det_eq_det_toMatrix_of_finset det_toMatrix_eq_det_toMatrix
det_toMatrix' 📖	mathematical	—	Matrix.det DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix addCommMonoid Matrix.addCommMonoid module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' MonoidHom AddCommGroup.toAddCommMonoid Pi.addCommGroup Ring.toAddCommGroup CommRing.toRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass det_toMatrix Finite.of_fintype
det_toMatrix_eq_det_toMatrix 📖	mathematical	—	Matrix.det DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap AddCommGroup.toAddCommMonoid Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finite.of_fintype	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype linearMap_toMatrix_mul_basis_toMatrix basis_toMatrix_mul_linearMap_toMatrix Matrix.det_conj_of_mul_eq_one Module.Basis.toMatrix_mul_toMatrix Module.Basis.toMatrix_self
det_zero 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det instZero Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.finrank	—	smulCommClass_self zero_smul det_smul map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass mul_one
det_zero' 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	nonempty_fintype RingHomInvPair.ids smulCommClass_self Finite.of_fintype det_toMatrix map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Matrix.det_zero
equivOfIsUnitDet_apply 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det	LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv equivOfIsUnitDet instFunLike	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim RingHomInvPair.ids Module.nontrivial
finiteDimensional_of_det_ne_one 📖	mathematical	—	FiniteDimensional Field.toDivisionRing	—	finite_of_det_ne_one
finite_of_det_ne_one 📖	mathematical	—	Module.Finite CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	Module.Finite.of_basis Finite.of_fintype coe_det
free_of_det_ne_one 📖	mathematical	—	Module.Free CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	Module.Free.of_basis coe_det
isUnit_det 📖	mathematical	IsUnit LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Module.End.instMonoid	MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det	—	IsUnit.map MonoidHom.instMonoidHomClass
isUnit_iff_isUnit_det 📖	mathematical	—	IsUnit LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Module.End.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype isUnit_toMatrix_iff det_toMatrix Matrix.isUnit_iff_isUnit_det
range_lt_top_of_det_eq_zero 📖	mathematical	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder range RingHomSurjective.ids Top.top Submodule.instTop	—	finite_of_det_ne_one NeZero.one EuclideanDomain.toNontrivial RingHomSurjective.ids lt_top_iff_ne_top ker_eq_bot_iff_range_eq_top bot_lt_iff_ne_bot bot_lt_ker_of_det_eq_zero instIsDomain Module.Free.of_divisionRing

Matrix

Definitions

Name	Category	Theorems
indexEquivOfInv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_comm 📖	mathematical	—	det Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	det_mul mul_comm
det_comm' 📖	mathematical	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	det	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim det_submatrix_equiv_self submatrix_mul_equiv det_comm Equiv.coe_refl submatrix_id_id
det_conj_of_mul_eq_one 📖	mathematical	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	det	—	det_comm' mul_assoc one_mul
det_map 📖	mathematical	—	det EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe Matrix EquivLike.toFunLike	—	Function.smulCommClass Algebra.to_smulCommClass Pi.isScalarTower IsScalarTower.right RingHomInvPair.ids map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass LinearMap.toMatrix'_one LinearMap.toMatrix'_mul map_mul NonUnitalRingHomClass.toMulHomClass RingEquivClass.toNonUnitalRingHomClass AlgEquivClass.toRingEquivClass LinearMap.toMatrix'_toLin' LinearMap.det_toLin' LinearMap.det_map

Module.Basis

Definitions

Name	Category	Theorems
det 📖	CompOp	51 math math: det_comp_basis, Orientation.volumeForm_robust_neg, OrthonormalBasis.det_to_matrix_orthonormalBasis_of_same_orientation, det_reindex', isUnit_det, OrthonormalBasis.det_eq_neg_det_of_opposite_orientation, OrthonormalBasis.det_to_matrix_orthonormalBasis_of_opposite_orientation, det_isEmpty, det_adjustToOrientation, det_isUnitSMul, AddSubgroup.index_eq_natAbs_det, Orientation.volumeForm_def, orientation_eq_iff_det_pos, Orientation.volumeForm_robust, ZSpan.measureReal_fundamentalDomain, NumberField.det_basisOfFractionalIdeal_eq_absNorm, ZSpan.measure_fundamentalDomain, det_unitsSMul, smul_det, det_reindex_symm, MeasureTheory.Measure.addHaar_parallelepiped, AddSubgroup.relIndex_eq_abs_det, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, OrthonormalBasis.det_to_matrix_orthonormalBasis, det_map', det_reindex, InnerProductSpace.gramSchmidtOrthonormalBasis_det, AlternatingMap.eq_smul_basis_det, OrthonormalBasis.det_adjustToOrientation, Pi.basisFun_det, ZLattice.covolume_eq_det_mul_measureReal, det_comp, abs_det_adjustToOrientation, det_self, det_basis, det_inv, Orientation.volumeForm_robust', FractionalIdeal.abs_det_basis_change, det_mul_det, OrthonormalBasis.same_orientation_iff_det_eq_det, AddSubgroup.relIndex_eq_natAbs_det, det_unitsSMul_self, det_smul_mk_coord_eq_det_update, OrthonormalBasis.det_to_matrix_orthonormalBasis_real, det_map, Ideal.natAbs_det_basis_change, OrthonormalBasis.abs_det_adjustToOrientation, is_basis_iff_det, det_apply, Pi.basisFun_det_apply, Submodule.natAbs_det_basis_change

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_apply 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike det Matrix.det toMatrix	—	—
det_basis 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det LinearEquiv.toLinearMap RingHomInvPair.ids equiv Equiv.refl AlternatingMap NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike det Module.Basis instFunLike	—	RingHomCompTriple.ids RingHomInvPair.ids det_comp_basis
det_comp 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike det LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det	—	det_apply RingHomInvPair.ids smulCommClass_self Finite.of_fintype LinearMap.det_toMatrix Matrix.det_mul AddMonoid.nat_smulCommClass' toMatrix_eq_toMatrix_constr RingHomCompTriple.ids LinearMap.toMatrix_comp constr_comp
det_comp_basis 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike det LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Module.Basis instFunLike MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det LinearMap.comp RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids equiv Equiv.refl	—	RingHomCompTriple.ids RingHomInvPair.ids det_apply smulCommClass_self Finite.of_fintype LinearMap.det_toMatrix LinearMap.toMatrix_comp Matrix.det_mul LinearMap.toMatrix_basis_equiv Matrix.det_one mul_one Matrix.ext toMatrix_apply LinearMap.toMatrix_apply
det_inv 📖	mathematical	—	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units Units.instInv IsUnit.unit DFunLike.coe AlternatingMap AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike det Module.Basis instFunLike isUnit_det	—	isUnit_det Units.mul_eq_one_iff_inv_eq IsUnit.unit_spec RingHomInvPair.ids det_basis LinearEquiv.det_mul_det_symm
det_isEmpty 📖	mathematical	—	det AlternatingMap.constOfIsEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	AlternatingMap.ext Matrix.det_isEmpty
det_isUnitSMul 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe AlternatingMap AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike det Module.Basis instFunLike isUnitSMul Finset.prod CommRing.toCommMonoid Finset.univ	—	det_unitsSMul_self
det_map 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike det map LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm	—	RingHomInvPair.ids det_apply toMatrix_map
det_map' 📖	mathematical	—	det map CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AlternatingMap.compLinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearEquiv.symm	—	RingHomInvPair.ids AlternatingMap.ext det_map
det_mul_det 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule AlternatingMap.instFunLike det Module.Basis instFunLike	—	RingHomInvPair.ids equiv_apply det_comp det_basis mul_comm
det_ne_zero 📖	—	—	—	—	NeZero.one det_self
det_reindex 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike det reindex Equiv EquivLike.toFunLike Equiv.instEquivLike	—	det_apply toMatrix_reindex' Matrix.det_reindexAlgEquiv
det_reindex' 📖	mathematical	—	det reindex CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AlternatingMap.domDomCongr NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule	—	AlternatingMap.ext det_reindex
det_reindex_symm 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike det reindex Equiv.symm Equiv EquivLike.toFunLike Equiv.instEquivLike	—	det_reindex Function.comp_assoc Equiv.self_comp_symm
det_self 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike det Module.Basis instFunLike AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.det.congr_simp toMatrix_self Matrix.det_one
det_smul_mk_coord_eq_det_update 📖	mathematical	LinearIndependent CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Top.top Submodule.instTop Submodule.span Set.range	LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.to_smulCommClass Algebra.id DFunLike.coe AlternatingMap AlternatingMap.instFunLike det coord MultilinearMap.toLinearMap AlternatingMap.toMultilinearMap	—	ext Algebra.to_smulCommClass eq_or_ne mk_coord_apply_eq mul_one Function.update_eq_self mk_coord_apply_ne MulZeroClass.mul_zero AlternatingMap.map_eq_zero_of_eq Function.update_of_ne Function.update_self
det_unitsSMul 📖	mathematical	—	det unitsSMul CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AlternatingMap NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Units.val Units Units.instInv Finset.prod CommGroup.toCommMonoid Units.instCommGroupUnits CommRing.toCommMonoid Finset.univ	—	AlternatingMap.ext Algebra.to_smulCommClass RingHomInvPair.ids Matrix.det.congr_simp repr_unitsSMul Units.coe_prod Matrix.det_mul_column
det_unitsSMul_self 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike det Module.Basis instFunLike unitsSMul Finset.prod CommRing.toCommMonoid Finset.univ Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Matrix.det.congr_simp toMatrix_unitsSMul Matrix.det_diagonal Finset.prod_congr
isUnit_det 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe AlternatingMap AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike det Module.Basis instFunLike	—	is_basis_iff_det linearIndependent span_eq
is_basis_iff_det 📖	mathematical	—	LinearIndependent CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.span Set.range Top.top Submodule Submodule.instTop IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe AlternatingMap NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike det	—	Eq.ge det_apply RingHomInvPair.ids smulCommClass_self Finite.of_fintype Matrix.ext LinearMap.toMatrix_id_eq_basis_toMatrix LinearEquiv.isUnit_det AddMonoid.nat_smulCommClass' toMatrix_eq_toMatrix_constr map_apply LinearEquiv.ofIsUnitDet_apply constr_basis linearIndependent span_eq
smul_det 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike det Module.Basis instSMul Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—

Module.Free

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_det_ne_one 📖	mathematical	—	Module.Free CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	of_basis LinearMap.coe_det

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basisFun_det 📖	mathematical	—	Module.Basis.det addCommGroup Ring.toAddCommGroup CommRing.toRing Function.module CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule basisFun Finite.of_fintype Matrix.detRowAlternating	—	AlternatingMap.ext Finite.of_fintype Module.Basis.det_apply Module.Basis.coePiBasisFun.toMatrix_eq_transpose Matrix.det_transpose Matrix.det.eq_1
basisFun_det_apply 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid addCommGroup Ring.toAddCommGroup CommRing.toRing Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AlternatingMap.instFunLike Module.Basis.det basisFun Finite.of_fintype Matrix.det Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.of	—	Finite.of_fintype basisFun_det

(root)

Definitions

Name	Category	Theorems
equivOfPiLEquivPi 📖	CompOp	—

---

← Back to Index