Basic

📁 Source: Mathlib/RingTheory/Norm/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems norm_gen_eq_coeff_zero_minpoly, norm_gen_eq_prod_roots, norm_eq_of_algEquiv, norm_eq_of_equiv_equiv, norm_eq_of_ringEquiv, norm_eq_prod_embeddings_gen, norm_eq_zero_iff, norm_eq_zero_iff', norm_eq_zero_iff_of_basis, norm_inv, norm_ne_zero_iff, norm_ne_zero_iff_of_basis, norm_zero, prod_embeddings_eq_finrank_pow, norm_gen_eq_one, norm_gen_eq_prod_roots	16
Total	16

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_eq_of_algEquiv 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike norm AlgEquiv AlgEquiv.instFunLike	—	smulCommClass_self IsScalarTower.left RingHomCompTriple.ids RingHomInvPair.ids LinearMap.det_conj LinearMap.ext map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgEquiv.apply_symm_apply
norm_eq_of_equiv_equiv 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring algebraMap RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.instFunLike norm RingEquiv.symm	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.injective map_mul NonUnitalRingHomClass.toMulHomClass RingEquivClass.toNonUnitalRingHomClass RingEquiv.symm_apply_apply commutes RingEquiv.map_mul' RingEquiv.map_add' norm_eq_of_ringEquiv norm_eq_of_algEquiv
norm_eq_of_ringEquiv 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring algebraMap RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.instFunLike norm	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass norm_eq_matrix_det smul_def RingEquiv.apply_symm_apply RingEquiv.map_det Matrix.ext RingHomInvPair.ids smulCommClass_self Finite.of_fintype to_smulCommClass IsScalarTower.right LinearEquiv.map_zero LinearMap.toMatrix_apply Module.Basis.coe_mapCoeffs norm_eq_one_of_not_exists_basis map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
norm_eq_prod_embeddings_gen 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring algebraMap minpoly PowerBasis.gen IsSeparable	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Ring.toSemiring MonoidHom.instFunLike norm Finset.prod AlgHom EuclideanDomain.toCommRing Field.toEuclideanDomain CommRing.toCommMonoid Finset.univ PowerBasis.AlgHom.fintype instIsDomain AlgHom.funLike	—	instIsDomain PowerBasis.norm_gen_eq_prod_roots Fintype.prod_equiv Finset.prod_mem_multiset Finset.prod_eq_multiset_prod Multiset.toFinset_val Multiset.dedup_eq_self Polynomial.nodup_roots Polynomial.Separable.map Multiset.map_id
norm_eq_zero_iff 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike norm MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	norm_eq_matrix_det Matrix.exists_mulVec_eq_zero_iff mul_eq_zero IsDomain.to_noZeroDivisors Module.Basis.ext_elem RingHomInvPair.ids map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass leftMulMatrix_mulVec_repr Finite.of_fintype Module.Basis.equivFun_apply Module.Basis.equivFun_symm_apply LinearEquiv.apply_symm_apply Mathlib.Tactic.Contrapose.contrapose₄ LinearEquiv.injective norm_zero IsDomain.toNontrivial
norm_eq_zero_iff' 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Ring.toAddCommGroup toModule Ring.toSemiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike LinearMap.mul to_smulCommClass IsScalarTower.right MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	norm_eq_zero_iff
norm_eq_zero_iff_of_basis 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike norm MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	norm_eq_zero_iff Module.Free.of_basis Module.Finite.of_basis
norm_inv 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidHom.instFunLike norm InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield	—	inv_zero norm_zero IsLocalRing.toNontrivial Field.instIsLocalRing Module.Free.of_divisionRing mul_left_injective₀ IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero instIsDomain norm_ne_zero_iff MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass inv_mul_cancel₀ map_one MonoidHomClass.toOneHomClass
norm_ne_zero_iff 📖	—	—	—	—	not_iff_not norm_eq_zero_iff
norm_ne_zero_iff_of_basis 📖	—	—	—	—	not_iff_not norm_eq_zero_iff_of_basis
norm_zero 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike norm MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim smulCommClass_self IsScalarTower.left norm_apply to_smulCommClass IsScalarTower.right coe_lmul_eq_mul map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass LinearMap.det_zero' Finite.of_fintype Module.Free.instNonemptyChooseBasisIndexOfNontrivial
prod_embeddings_eq_finrank_pow 📖	mathematical	—	Finset.prod AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Finset.univ minpoly.AlgHom.fintype DivisionRing.toRing Field.toDivisionRing instIsDomain DFunLike.coe AlgHom.funLike RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap PowerBasis.gen Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommRing.toCommSemiring Ring.toSemiring PowerBasis.AlgHom.fintype Module.finrank NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule	—	instIsDomain FiniteDimensional.right Fintype.prod_equiv Finset.univ_sigma_univ Finset.prod_sigma Finset.prod_pow Finset.prod_congr Finset.prod_const AlgHom.card isSeparable_tower_top_of_isSeparable

Algebra.PowerBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_gen_eq_coeff_zero_minpoly 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike Algebra.norm PowerBasis.gen Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne PowerBasis.dim Polynomial.coeff minpoly	—	Algebra.norm_eq_matrix_det Matrix.det_eq_sign_charpoly_coeff charpoly_leftMulMatrix Fintype.card_fin
norm_gen_eq_prod_roots 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring algebraMap minpoly PowerBasis.gen	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Ring.toSemiring MonoidHom.instFunLike Algebra.norm Multiset.prod CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.aroots instIsDomain	—	minpoly.monic PowerBasis.isIntegral_gen instIsDomain norm_gen_eq_coeff_zero_minpoly PowerBasis.natDegree_minpoly Module.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Polynomial.coeff_map Polynomial.Splits.coeff_zero_eq_prod_roots_of_monic Polynomial.Monic.map Polynomial.Monic.natDegree_map map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass mul_assoc mul_pow map_neg RingHomClass.toAddMonoidHomClass map_one MonoidHomClass.toOneHomClass neg_mul one_mul neg_neg one_pow

IntermediateField.AdjoinSimple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_gen_eq_one 📖	mathematical	IsIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	DFunLike.coe MonoidHom IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring IntermediateField.toField CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike Algebra.norm IntermediateField.algebra' Algebra.toSMul Semifield.toCommSemiring Field.toSemifield Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule gen AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	IsScalarTower.left Algebra.norm_eq_one_of_not_exists_basis Mathlib.Tactic.Contrapose.contrapose₄ IsIntegral.of_mem_of_fg Submodule.fg_iff_finiteDimensional Module.Basis.finiteDimensional_of_finite Finite.of_fintype IntermediateField.subset_adjoin Set.mem_singleton
norm_gen_eq_prod_roots 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map CommSemiring.toSemiring Semifield.toCommSemiring algebraMap minpoly EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MonoidHom IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Ring.toSemiring IntermediateField.toField CommRing.toCommSemiring MonoidHom.instFunLike Algebra.norm IntermediateField.algebra' Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule gen Multiset.prod CommRing.toCommMonoid Polynomial.aroots instIsDomain	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing IsScalarTower.left instIsDomain IntermediateField.adjoin.powerBasis_gen Algebra.PowerBasis.norm_gen_eq_prod_roots minpoly.algebraMap_eq IntermediateField.isScalarTower_mid' algebraMap_gen Polynomial.aroots.congr_simp norm_gen_eq_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass minpoly.eq_zero Polynomial.roots.congr_simp Polynomial.map_zero Polynomial.roots_zero

---

← Back to Index