NormDeterminant

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

Statistics

Metric	Count
Definitions	0
Theorems det_toLinearMap_eq_norm	1
Total	1

QuadraticAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_toLinearMap_eq_norm 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring QuadraticAlgebra AddCommGroup.toAddCommMonoid instAddCommGroup Ring.toAddCommGroup CommRing.toRing instModule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det DistribSMul.toLinearMap instAddCommMonoid NonUnitalNonAssocSemiring.toDistribSMul instNonUnitalNonAssocSemiring IsScalarTower.to_smulCommClass' instCommSemiring instAlgebra Algebra.id IsScalarTower.right instNonAssocSemiring norm	—	IsScalarTower.to_smulCommClass' IsScalarTower.right RingHomInvPair.ids smulCommClass_self Finite.of_fintype LinearMap.det_toMatrix Matrix.det_fin_two_of Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right 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_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_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.add_pf_add_gt LinearEquiv.eq_symm_apply LinearMap.ext LinearEquiv.injective DFunLike.coe_injective' LinearMap.toMatrix_symm Matrix.repr_toLin Fintype.complete Matrix.mulVec_cons add_zero Matrix.tail_cons Matrix.cons_val_fin_one

---

← Back to Index