NormTrace

📁 Source: Mathlib/RingTheory/Localization/NormTrace.lean

Statistics

Metric	Count
Definitions	0
Theorems discr_localizationLocalization, map_leftMulMatrix_localization, norm_eq_iff, norm_localization, traceMatrix_localizationLocalization, trace_localization	6
Total	6

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discr_localizationLocalization 📖	mathematical	—	discr DFunLike.coe Module.Basis CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule Module.Basis.instFunLike Module.Basis.localizationLocalization RingHom RingHom.instFunLike algebraMap NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	discr_def RingHom.map_det traceMatrix_localizationLocalization
map_leftMulMatrix_localization 📖	mathematical	—	DFunLike.coe RingHom Matrix Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike RingHom.mapMatrix algebraMap AlgHom Matrix.semiring Matrix.instAlgebra id AlgHom.funLike leftMulMatrix Module.Basis.localizationLocalization	—	Matrix.ext RingHomInvPair.ids leftMulMatrix_eq_repr_mul Module.Basis.localizationLocalization_apply NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Module.Basis.localizationLocalization_repr_algebraMap
norm_eq_iff 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero	DFunLike.coe MonoidHom MulOneClass.toMulOne Ring.toSemiring CommRing.toRing MonoidHom.instFunLike norm RingHom RingHom.instFunLike algebraMap	—	norm_localization IsLocalization.injective
norm_localization 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike norm RingHom RingHom.instFunLike algebraMap	—	subsingleton_or_nontrivial Module.subsingleton norm_eq_matrix_det RingHom.map_det map_leftMulMatrix_localization
traceMatrix_localizationLocalization 📖	mathematical	—	traceMatrix DFunLike.coe Module.Basis CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule Module.Basis.instFunLike Module.Basis.localizationLocalization RingHom Matrix Matrix.nonAssocSemiring RingHom.instFunLike RingHom.mapMatrix algebraMap NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Module.Finite.of_basis Finite.of_fintype Module.Free.of_basis Matrix.ext Module.Basis.localizationLocalization_apply NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass trace_localization
trace_localization 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule Semiring.toModule LinearMap.instFunLike trace RingHom RingHom.instFunLike algebraMap	—	subsingleton_or_nontrivial Module.subsingleton trace_eq_matrix_trace map_leftMulMatrix_localization AddMonoidHom.map_trace AddMonoidHom.instAddMonoidHomClass

---

← Back to Index