Norm

📁 Source: Mathlib/LinearAlgebra/FreeModule/Norm.lean

Statistics

Metric	Count
Definitions	0
Theorems associated_norm_prod_smith, finrank_quotient_span_eq_natDegree_norm, instFiniteDimensionalQuotientPolynomialIdealSpanSingletonSetSmithCoeffs	3
Total	3

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associated_norm_prod_smith 📖	mathematical	—	Associated MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing MonoidHom.instFunLike Algebra.norm Finset.prod CommRing.toCommMonoid Finset.univ Ideal.smithCoeffs Finite.of_fintype Ideal.span Set Set.instSingletonSet Ideal Bot.bot Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Iff.not Ideal.span_singleton_eq_bot	—	Iff.not Ideal.span_singleton_eq_bot Finite.of_fintype Matrix.det_diagonal RingHomInvPair.ids smulCommClass_self LinearMap.det_toLin IsScalarTower.right RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul Submodule.isScalarTower' instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors NoZeroDivisors.toNoZeroSMulDivisors IsDomain.to_noZeroDivisors Associated.symm LinearMap.associated_det_of_eq_comp Module.Basis.ext Matrix.toLin_apply Finset.sum_congr Module.Basis.repr_self Finsupp.single_eq_pi_single Matrix.diagonal_mulVec_single Pi.single_apply ite_smul zero_smul Finset.sum_ite_eq' mul_one Finset.mem_univ Module.Basis.equiv_apply mul_comm smul_eq_mul LinearEquiv.restrictScalars_apply
finrank_quotient_span_eq_natDegree_norm 📖	mathematical	—	Module.finrank HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.span Set Set.instSingletonSet DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Submodule.Quotient.module' CommRing.toRing Ring.toAddCommGroup Semiring.toModule Algebra.toSMul Semifield.toCommSemiring Algebra.toModule IsScalarTower.right Polynomial.natDegree DFunLike.coe MonoidHom Polynomial MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidHom.instFunLike Algebra.norm	—	Iff.not Ideal.span_singleton_eq_bot IsScalarTower.right Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd instIsDomain EuclideanDomain.to_principal_ideal_domain Finite.of_fintype Polynomial.natDegree_eq_of_degree_eq Polynomial.degree_eq_degree_of_associated associated_norm_prod_smith Polynomial.natDegree_prod IsDomain.to_noZeroDivisors Ideal.smithCoeffs_ne_zero Ideal.finrank_quotient_eq_sum IsLocalRing.toNontrivial Field.instIsLocalRing Module.free_of_finite_type_torsion_free' instFiniteDimensionalQuotientPolynomialIdealSpanSingletonSetSmithCoeffs instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors PowerBasis.finrank commRing_strongRankCondition
instFiniteDimensionalQuotientPolynomialIdealSpanSingletonSetSmithCoeffs 📖	mathematical	—	FiniteDimensional HasQuotient.Quotient Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Ideal Polynomial.semiring Ideal.instHasQuotient_1 Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain Ideal.span Set Set.instSingletonSet Ideal.smithCoeffs Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing instIsDomain EuclideanDomain.to_principal_ideal_domain Polynomial.instEuclideanDomain Submodule.Quotient.addCommGroup Polynomial.ring Ring.toAddCommGroup Semiring.toModule Submodule.Quotient.module' DivisionRing.toDivisionSemiring Algebra.toSMul Semifield.toCommSemiring Polynomial.algebraOfAlgebra Algebra.id Polynomial.module IsScalarTower.right	—	PowerBasis.finite Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd instIsDomain EuclideanDomain.to_principal_ideal_domain Ideal.smithCoeffs_ne_zero

---

← Back to Index