Basic

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

Statistics

Metric	Count
Definitions instField, instStar, instStarRing, norm, omega, termω	6
Theorems algHom_ext, algHom_ext_iff, algebraMap_mem_nonZeroDivisors_iff, algebraMap_norm_eq_mul_star, coe_mem_nonZeroDivisors_iff, coe_norm_eq_mul_star, im_star, isUnit_iff_norm_isUnit, lift_apply_apply, lift_symm_apply_coe, mem_unitary, mk_eq_add_smul_omega, mker_norm_eq_unitary, mul_star, norm_algebraMap, norm_coe, norm_def, norm_eq_one, norm_eq_one_iff_mem_unitary, norm_eq_zero_iff_eq_zero, norm_intCast, norm_mem_nonZeroDivisors_iff, norm_natCast, norm_neg, norm_one, norm_star, norm_zero, omega_im, omega_mul_algebraMap_mul_mk, omega_mul_coe_mul_mk, omega_mul_mk, omega_mul_omega_eq_add, omega_mul_omega_eq_mk, omega_re, re_star, star_mem_nonZeroDivisors, star_mem_nonZeroDivisors_iff, star_mk	38
Total	44

QuadraticAlgebra

Definitions

Name	Category	Theorems
instField 📖	CompOp	—
instStar 📖	CompOp	9 math math: star_mem_nonZeroDivisors_iff, star_mk, mul_star, coe_norm_eq_mul_star, re_star, star_mem_nonZeroDivisors, norm_star, algebraMap_norm_eq_mul_star, im_star
instStarRing 📖	CompOp	3 math math: norm_eq_one_iff_mem_unitary, mem_unitary, mker_norm_eq_unitary
norm 📖	CompOp	18 math math: norm_algebraMap, norm_zero, norm_eq_one_iff_mem_unitary, norm_eq_one, norm_neg, norm_natCast, norm_coe, isUnit_iff_norm_isUnit, coe_norm_eq_mul_star, norm_intCast, mker_norm_eq_unitary, norm_def, norm_one, norm_star, algebraMap_norm_eq_mul_star, det_toLinearMap_eq_norm, norm_mem_nonZeroDivisors_iff, norm_eq_zero_iff_eq_zero
omega 📖	CompOp	10 math math: omega_mul_coe_mul_mk, lift_symm_apply_coe, omega_mul_omega_eq_mk, omega_re, omega_mul_algebraMap_mul_mk, algHom_ext_iff, omega_im, mk_eq_add_smul_omega, omega_mul_mk, omega_mul_omega_eq_add
termω 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algHom_ext 📖	—	DFunLike.coe AlgHom QuadraticAlgebra CommSemiring.toSemiring instCommSemiring Ring.toSemiring instAlgebra Algebra.id AlgHom.funLike omega MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	AlgHom.ext mk_eq_add_smul_omega map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass AlgHom.commutes map_smul SemilinearMapClass.toMulActionSemiHomClass
algHom_ext_iff 📖	mathematical	—	DFunLike.coe AlgHom QuadraticAlgebra CommSemiring.toSemiring instCommSemiring Ring.toSemiring instAlgebra Algebra.id AlgHom.funLike omega MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	algHom_ext
algebraMap_mem_nonZeroDivisors_iff 📖	mathematical	—	QuadraticAlgebra Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring instCommSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap instAlgebra Algebra.id	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass MulZeroClass.mul_zero add_zero zero_add im_zero re_zero ext_iff
algebraMap_norm_eq_mul_star 📖	mathematical	—	DFunLike.coe RingHom QuadraticAlgebra Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommSemiring RingHom.instFunLike algebraMap instAlgebra Algebra.id MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring MonoidHom.instFunLike norm instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd Star.star instStar	—	ext mul_comm map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_add AddMonoidHomClass.toAddHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass MulZeroClass.mul_zero add_zero mul_neg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_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.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_congr sub_self Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
coe_mem_nonZeroDivisors_iff 📖	mathematical	—	QuadraticAlgebra Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring instCommSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap instAlgebra Algebra.id	—	algebraMap_mem_nonZeroDivisors_iff
coe_norm_eq_mul_star 📖	mathematical	—	DFunLike.coe RingHom QuadraticAlgebra Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommSemiring RingHom.instFunLike algebraMap instAlgebra Algebra.id MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring MonoidHom.instFunLike norm instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd Star.star instStar	—	algebraMap_norm_eq_mul_star
im_star 📖	mathematical	—	im Star.star QuadraticAlgebra instStar NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	—
isUnit_iff_norm_isUnit 📖	mathematical	—	IsUnit QuadraticAlgebra MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring instCommSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring Semiring.toNonAssocSemiring MonoidHom.instFunLike norm	—	IsUnit.map MonoidHom.instMonoidHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_assoc algebraMap_norm_eq_mul_star C_eq_algebraMap C_mul mul_comm
lift_apply_apply 📖	mathematical	—	DFunLike.coe AlgHom QuadraticAlgebra CommSemiring.toSemiring instCommSemiring Ring.toSemiring instAlgebra Algebra.id AlgHom.funLike Equiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toAdd Algebra.toSMul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne EquivLike.toFunLike Equiv.instEquivLike lift re im	—	—
lift_symm_apply_coe 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toAdd Algebra.toSMul Ring.toSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DFunLike.coe Equiv AlgHom QuadraticAlgebra CommSemiring.toSemiring instCommSemiring instAlgebra Algebra.id EquivLike.toFunLike Equiv.instEquivLike Equiv.symm lift AlgHom.funLike omega MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
mem_unitary 📖	mathematical	DFunLike.coe MonoidHom QuadraticAlgebra MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike norm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero instCommSemiring SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring instStarRing	—	norm_eq_one_iff_mem_unitary
mk_eq_add_smul_omega 📖	mathematical	—	QuadraticAlgebra instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe RingHom instCommSemiring RingHom.instFunLike algebraMap instAlgebra Algebra.id instSMul Algebra.toSMul omega MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	ext MulZeroClass.mul_zero add_zero mul_one zero_add
mker_norm_eq_unitary 📖	mathematical	—	MonoidHom.mker QuadraticAlgebra MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom MulOneClass.toMulOne MonoidHom.instFunLike MonoidHom.instMonoidHomClass norm unitary MonoidWithZero.toMonoid Semiring.toMonoidWithZero instCommSemiring StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring instStarRing	—	Submonoid.ext MonoidHom.instMonoidHomClass norm_eq_one_iff_mem_unitary
mul_star 📖	mathematical	—	QuadraticAlgebra instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd Star.star instStar instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing instAdd DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommSemiring RingHom.instFunLike algebraMap instAlgebra Algebra.id	—	ext mul_neg MulZeroClass.mul_zero add_zero MulZeroClass.zero_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf 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 Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf sub_self Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero
norm_algebraMap 📖	mathematical	—	DFunLike.coe MonoidHom QuadraticAlgebra MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike norm RingHom instCommSemiring RingHom.instFunLike algebraMap instAlgebra Algebra.id Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	MulZeroClass.mul_zero add_zero sub_zero pow_two
norm_coe 📖	mathematical	—	DFunLike.coe MonoidHom QuadraticAlgebra MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike norm RingHom instCommSemiring RingHom.instFunLike algebraMap instAlgebra Algebra.id Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	norm_algebraMap
norm_def 📖	mathematical	—	DFunLike.coe MonoidHom QuadraticAlgebra MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike norm SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul re im	—	—
norm_eq_one 📖	mathematical	QuadraticAlgebra Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring instCommSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring instStarRing	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring Semiring.toNonAssocSemiring MonoidHom.instFunLike norm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	norm_eq_one_iff_mem_unitary
norm_eq_one_iff_mem_unitary 📖	mathematical	—	DFunLike.coe MonoidHom QuadraticAlgebra MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike norm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero instCommSemiring SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring instStarRing	—	Unitary.mem_iff_self_mul_star algebraMap_norm_eq_mul_star map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
norm_eq_zero_iff_eq_zero 📖	mathematical	—	DFunLike.coe MonoidHom QuadraticAlgebra MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidHom.instFunLike norm MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instZero	—	ext MulZeroClass.mul_zero add_zero sub_zero IsDomain.to_noZeroDivisors instIsDomain norm_def Fact.out eq_sub_iff_add_eq sub_eq_zero pow_two norm_zero
norm_intCast 📖	mathematical	—	DFunLike.coe MonoidHom QuadraticAlgebra MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike norm AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing instCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	MulZeroClass.mul_zero add_zero sub_zero pow_two
norm_mem_nonZeroDivisors_iff 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors DFunLike.coe MonoidHom QuadraticAlgebra MulOneClass.toMulOne NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring Semiring.toNonAssocSemiring MonoidHom.instFunLike norm instCommSemiring	—	C_mul_eq_smul C_eq_algebraMap algebraMap_norm_eq_mul_star mul_comm mul_assoc MulZeroClass.zero_mul ext algebraMap_mem_nonZeroDivisors_iff Submonoid.mul_mem star_mem_nonZeroDivisors
norm_natCast 📖	mathematical	—	DFunLike.coe MonoidHom QuadraticAlgebra MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike norm AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing instCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	MulZeroClass.mul_zero add_zero sub_zero pow_two
norm_neg 📖	mathematical	—	DFunLike.coe MonoidHom QuadraticAlgebra MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike norm instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	mul_neg neg_mul neg_neg
norm_one 📖	mathematical	—	DFunLike.coe MonoidHom QuadraticAlgebra MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike norm instOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	mul_one MulZeroClass.mul_zero add_zero sub_zero
norm_star 📖	mathematical	—	DFunLike.coe MonoidHom QuadraticAlgebra MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike norm Star.star instStar	—	mul_neg neg_mul neg_neg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf 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 Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero
norm_zero 📖	mathematical	—	DFunLike.coe MonoidHom QuadraticAlgebra MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidHom.instFunLike norm instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	MulZeroClass.mul_zero add_zero sub_self
omega_im 📖	mathematical	—	im omega	—	—
omega_mul_algebraMap_mul_mk 📖	mathematical	—	QuadraticAlgebra instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd omega MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DFunLike.coe RingHom instCommSemiring RingHom.instFunLike algebraMap instAlgebra Algebra.id	—	ext MulZeroClass.zero_mul mul_one MulZeroClass.mul_zero add_zero one_mul zero_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf 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
omega_mul_coe_mul_mk 📖	mathematical	—	QuadraticAlgebra instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd omega MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DFunLike.coe RingHom instCommSemiring RingHom.instFunLike algebraMap instAlgebra Algebra.id	—	—
omega_mul_mk 📖	mathematical	—	QuadraticAlgebra instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd omega MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	ext MulZeroClass.zero_mul mul_one zero_add one_mul
omega_mul_omega_eq_add 📖	mathematical	—	QuadraticAlgebra instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd omega MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instAdd instSMul Algebra.toSMul Algebra.id instOne	—	ext MulZeroClass.mul_zero mul_one zero_add add_zero
omega_mul_omega_eq_mk 📖	mathematical	—	QuadraticAlgebra instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd omega MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	ext MulZeroClass.mul_zero mul_one zero_add add_zero
omega_re 📖	mathematical	—	re omega	—	—
re_star 📖	mathematical	—	re Star.star QuadraticAlgebra instStar Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul im	—	—
star_mem_nonZeroDivisors 📖	mathematical	QuadraticAlgebra Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring instCommSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	Star.star instStar	—	mem_nonZeroDivisors_iff_right Function.Involutive.injective InvolutiveStar.star_involutive star_zero StarMul.star_mul mul_comm
star_mem_nonZeroDivisors_iff 📖	mathematical	—	QuadraticAlgebra Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring instCommSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors Star.star instStar	—	InvolutiveStar.star_involutive star_mem_nonZeroDivisors
star_mk 📖	mathematical	—	Star.star QuadraticAlgebra instStar Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	—

---

← Back to Index