Basic

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

Statistics

Metric	Count
Definitions subInvSMul, resolvent, resolventSet, spectrum	4
Theorems spectrum_eq, apply_mem_spectrum, mem_resolventSet_apply, spectrum_apply_subset, val_inv_subInvSMul, val_subInvSMul, zero_notMem_spectrum, resolventSet_neg, add_mem_add_iff, add_mem_iff, add_singleton_eq, algebraMap_mem, algebraMap_mem_iff, inv_mem_iff, inv_mem_resolventSet, inv₀_mem, inv₀_mem_iff, inv₀_mem_inv, inv₀_mem_inv_iff, isUnit_of_zero_notMem, isUnit_resolvent, map_inv, map_star, mem_iff, mem_resolventSet_iff, mem_resolventSet_of_left_right_inverse, ne_zero_of_mem_of_unit, neg_eq, nonzero_mul_comm, notMem_iff, not_isUnit_of_zero_mem, of_algebraMap_mem, of_inv₀_mem, of_inv₀_mem_inv, of_subsingleton, one_eq, preimage_algebraMap, preimage_units_mul_comm, resolventSet_of_subsingleton, resolvent_eq, scalar_eq, setOf_isUnit_inter_mul_comm, singleton_add_eq, singleton_sub_eq, smul_eq_smul, smul_mem_smul_iff, star_mem_resolventSet_iff, sub_singleton_eq, subset_singleton_zero_compl, subset_subalgebra, unit_mem_mul_comm, unit_smul_eq_smul, units_conjugate, units_conjugate', units_smul_resolvent, units_smul_resolvent_self, vadd_eq, zero_eq, zero_mem, zero_mem_iff, zero_mem_resolventSet_of_unit, zero_notMem, zero_notMem_iff	63
Total	67

AlgEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
spectrum_eq 📖	mathematical	—	spectrum DFunLike.coe EquivLike.toFunLike	—	Set.Subset.antisymm AlgHom.spectrum_apply_subset AlgEquivClass.toAlgHomClass coe_coe_symm_apply_coe_apply instAlgEquivClass

AlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_mem_spectrum 📖	mathematical	—	Set Set.instMembership spectrum CommRing.toCommSemiring DFunLike.coe	—	RingHom.instRingHomClass AlgHomClass.toRingHomClass map_sub RingHomClass.toAddMonoidHomClass AlgHomClass.commutes sub_self coe_subset_nonunits RingHom.ker_ne_top
mem_resolventSet_apply 📖	mathematical	Set Set.instMembership resolventSet	Set Set.instMembership resolventSet DFunLike.coe	—	map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass instNonUnitalAlgHomClassOfAlgHomClass AlgHomClass.commutes IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass
spectrum_apply_subset 📖	mathematical	—	Set Set.instHasSubset spectrum DFunLike.coe	—	mem_resolventSet_apply

IsUnit

Definitions

Name	Category	Theorems
subInvSMul 📖	CompOp	2 math math: val_subInvSMul, val_inv_subInvSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
val_inv_subInvSMul 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Units CommSemiring.toSemiring Units.instSMul Algebra.toSMul DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Units Units.instInv subInvSMul CommSemiring.toSemiring Units.instSMul Algebra.toSMul unit SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	—
val_subInvSMul 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Units CommSemiring.toSemiring Units.instSMul Algebra.toSMul DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring subInvSMul SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap Units Units.instSMul Algebra.toSMul Units.instInv	—	—

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
zero_notMem_spectrum 📖	mathematical	—	Set Set.instMembership spectrum val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	spectrum.zero_notMem isUnit

(root)

Definitions

Name	Category	Theorems
resolvent 📖	CompOp	11 math math: spectrum.units_smul_resolvent_self, spectrum.resolvent_eq, spectrum.eventually_isUnit_resolvent, spectrum.hasDerivAt_resolvent, spectrum.hasFDerivAt_resolvent, spectrum.resolvent_tendsto_cobounded, spectrum.hasDerivAt_resolvent_const_right, spectrum.hasDerivAt_resolvent_const_left, spectrum.units_smul_resolvent, spectrum.resolvent_isBigO_inv, spectrum.isUnit_resolvent
resolventSet 📖	CompOp	14 math math: spectrum.isOpen_resolventSet, spectrum.mem_resolventSet_of_left_right_inverse, IsCompactOperator.hasEigenvalue_or_mem_resolventSet, spectrum.zero_mem_resolventSet_of_unit, spectrum.mem_resolventSet_iff, spectrum.star_mem_resolventSet_iff, resolventSet_neg, spectrum.mem_resolventSet_of_norm_lt, spectrum.inv_mem_resolventSet, AlgHom.mem_resolventSet_apply, spectrum.mem_resolventSet_of_spectralRadius_lt, spectrum.resolventSet_of_subsingleton, spectrum.isUnit_resolvent, spectrum.mem_resolventSet_of_norm_lt_mul
spectrum 📖	CompOp	241 math math: unitary.spectrum.unitary_conjugate, spectrum.inv_mem_iff, quasispectrum_eq_spectrum_union, spectrum_subset_quasispectrum, Matrix.IsHermitian.isClosedEmbedding_cfcAux, IsometricContinuousFunctionalCalculus.isGreatest_nnnorm_spectrum, IsSelfAdjoint.commute_cfcHom, cfcHom_injective, Subalgebra.spectrum_sUnion_connectedComponentIn, Module.End.HasEigenvalue.mem_spectrum, spectrum.subset_closedBall_norm_mul, spectrumRestricts_iff, spectrum.instCompactSpace, spectrum.of_inv₀_mem, Matrix.spectrum_toEuclideanLin, spectrum.inv₀_mem_iff, ContinuousFunctionalCalculus.compactSpace_spectrum, IsIdempotentElem.finite_spectrum, Module.End.spectrum_intrinsicStar, CStarAlgebra.norm_or_neg_norm_mem_spectrum, Matrix.spectrum_toLpLin, StarAlgebra.elemental.characterSpaceToSpectrum_coe, WeakDual.CharacterSpace.apply_mem_spectrum, Matrix.mem_spectrum_iff_isRoot_charpoly, cfcHom_mem_elemental, cfcHom_continuous, cfcL_apply, LinearMap.spectrum_toMatrix', spectrum.nonempty_of_isAlgClosed_of_finiteDimensional, cfcHom_nonneg_iff, cfc_apply_mkD, spectrum_diagonal, unitary.spectrum.unitary_conjugate', spectrum.pow_mem_pow, AlgHom.apply_mem_spectrum, NNReal.spectrum_nonempty, cfcHom_isClosedEmbedding, SpectrumRestricts.compactSpace, cfcL_integrable, IsGreatest.nnnorm_cfc_nnreal, Pi.spectrum_eq, spectrum.zero_notMem_iff, ContinuousFunctionalCalculus.isCompact_spectrum, IsIdempotentElem.spectrum_subset, cfcHom_le_iff, cfcHom_id, Unitary.spectrum_star_left_conjugate, IsSelfAdjoint.coe_mem_spectrum_complex, spectrum.zero_mem_iff, spectrum.gelfandTransform_eq, spectrum.zero_mem, spectrum.zero_notMem, cfc_map_spectrum, ContinuousMap.spectrum_eq_preimage_range, Matrix.mem_spectrum_of_isRoot_charpoly, Unitary.norm_sub_one_lt_two_iff, spectrum.isCompact, spectrum.algebraMap_mem_iff, CFC.spectrum_algebraMap_eq, SpectrumRestricts.isClosedEmbedding_starAlgHom, SpectrumRestricts.algebraMap_image, continuousOn_cfc_setProd, IsGreatest.norm_cfc, spectrum.smul_mem_smul_iff, Matrix.finite_spectrum, IsSelfAdjoint.val_re_map_spectrum, Unitization.zero_mem_spectrum_inr, Module.End.hasUnifEigenvalue_iff_mem_spectrum, coe_mem_spectrum_real_of_nonneg, SpectrumRestricts.continuous_starAlgHom, IsGreatest.nnnorm_cfc, Prod.spectrum_eq, IsSelfAdjoint.isConnected_spectrum_compl, spectrum.one_eq, Matrix.instFiniteSpectrum, StarAlgebra.elemental.bijective_characterSpaceToSpectrum, Unitary.spectrum_star_right_conjugate, continuousOn_cfc_nnreal, cfcHom_integral, spectrum.map_pow, ContinuousFunctionalCalculus.exists_cfc_of_predicate, spectrum.pow_image_subset, Real.spectralRadius_mem_spectrum, spectrum.units_conjugate, Units.continuousOn_zpow₀_spectrum, spectrum.subset_subalgebra, cfc_def, IsSelfAdjoint.spectrum_nonempty, lipschitzOnWith_cfc_fun, Subalgebra.spectrum_eq_of_isPreconnected_compl, cfcHom_comp, StarSubalgebra.spectrum_eq, spectrum.inv₀_mem_inv_iff, SpectrumRestricts.subset_preimage, Matrix.IsHermitian.cfcAux_apply, cfc_eq_cfc_iff_eqOn, spectrum_imaginaryPart, spectrum.preimage_algebraMap, Matrix.instFiniteElemRealSpectrum, unitary.spectrum_subset_circle, spectrum.map_pow_of_nonempty, spectrum.isClosed, Real.spectralRadius_mem_spectrum_or, mem_quasispectrum_iff, LinearMap.spectrum_toMatrix, cfcUnits_pow, spectrum.isBounded, Unitization.mem_spectrum_inr_of_not_isUnit, Subalgebra.frontier_subset_frontier, spectrum.exists_mem_of_not_isUnit_aeval_prod, spectrum.subset_singleton_zero_compl, spectrum.inv₀_mem, AlgEquiv.spectrum_eq, spectrum.nonempty, Subalgebra.spectrum_isBounded_connectedComponentIn, spectrum.map_polynomial_aeval_of_nonempty, spectrum_subset_unitary_of_mem_unitary, spectrum.add_singleton_eq, cfc_eq_cfcL_mkD, cfcHomSuperset_apply, range_cfc_eq_range_cfcHom, NormedRing.algEquivComplexOfComplete_symm_apply, Matrix.IsHermitian.spectrum_eq_image_range, Unitary.spectrum_subset_slitPlane_iff_norm_lt_two, isIdempotentElem_iff_spectrum_subset, spectrum.of_inv₀_mem_inv, spectrum.singleton_add_eq, spectrum.singleton_sub_eq, NNReal.spectralRadius_mem_spectrum, CFC.spectrum_rpow, spectrum.map_star, Module.End.finite_spectrum, eqOn_of_cfc_eq_cfc, upperHemicontinuous_spectrum_nnreal, spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty, spec_cfcₙAux, cfcHom_eq_cfc_extend, spectrum.subset_polynomial_aeval, SpectrumRestricts.apply_mem, Matrix.spectrum_toLin, SpectrumRestricts.starAlgHom_apply, Matrix.finite_real_spectrum, spectrum.map_inv, Commute.cfcHom, AlgHom.spectrum_apply_subset, cfc_apply, spectrum.mem_iff, spectrum.add_mem_add_iff, spectrum.map_polynomial_aeval_of_degree_pos, ContinuousMap.spectrum_eq_range, cfcL_integral, StarSubalgebra.mem_spectrum_iff, Matrix.IsHermitian.spectrum_real_eq_range_eigenvalues, isStarProjection_iff_spectrum_subset_and_isSelfAdjoint, cfcHom_isStrictlyPositive_iff, WeakDual.CharacterSpace.mem_spectrum_iff_exists, spectrum.add_mem_iff, CFC.spectrum_abs, Units.continuousOn_inv₀_spectrum, Units.zero_notMem_spectrum, cfc_apply_pi, SpectrumRestricts.image, spectrum.units_conjugate', range_cfcHom_le, IsSelfAdjoint.map_spectrum_real, ContinuousLinearMap.spectrum_eq, spectrum.exp_mem_exp, isStarProjection_iff_spectrum_subset_and_isStarNormal, Matrix.IsHermitian.cfcAux_id, spectrum.scalar_eq, unitary_iff_isStarNormal_and_spectrum_subset_unitary, spectrum.of_subsingleton, Subalgebra.frontier_spectrum, spectrum.setOf_isUnit_inter_mul_comm, Unitization.quasispectrum_eq_spectrum_inr', spectrum.isCompact_nnreal, spectrum.unit_mem_mul_comm, selfAdjoint.val_re_map_spectrum, Matrix.IsHermitian.eigenvalues_mem_spectrum_real, cfc_eq_cfcL, cfcHom_predicate, spectrum.instCompactSpaceNNReal, spectrum.preimage_units_mul_comm, norm_cfcHom, spectrum.exists_nnnorm_eq_spectralRadius, spectrum_realPart, spectrum.inv₀_mem_inv, unitary.norm_sub_one_lt_two_iff, spectrum_imaginaryPart', spectrum.nonzero_mul_comm, quasispectrum_eq_spectrum_union_zero, continuousOn_cfc_nnreal_setProd, SpectrumRestricts.rightInvOn, range_cfcHom, Module.End.mem_spectrum_iff_isRoot_charpoly, nnnorm_cfcHom, continuousOn_cfc, StarAlgebra.elemental.continuous_characterSpaceToSpectrum, spectrum.neg_eq, CStarAlgebra.norm_mem_spectrum_of_nonneg, Module.End.hasEigenvalue_iff_mem_spectrum, CFC.spectrum_one_eq, IsometricContinuousFunctionalCalculus.isGreatest_norm_spectrum, spectrum.algebraMap_mem, spectrum.unit_smul_eq_smul, CFC.spectrum_nonempty, CFC.spectrum_algebraMap_subset, spectrum.smul_eq_smul, spectrum_realPart', cfcHom_mono, IsometricContinuousFunctionalCalculus.isometric, spectrum.map_polynomial_aeval, ContinuousFunctionalCalculus.spectrum_nonempty, Unitization.quasispectrum_eq_spectrum_inr, spectrum.map_pow_of_pos, ClosedEmbeddingContinuousFunctionalCalculus.isClosedEmbedding, cfcHom_eq_of_isStarNormal, upperHemicontinuous_spectrum, spectrum.of_algebraMap_mem, cfcHom_map_spectrum, spectrum.zero_eq, spectrum.subset_circle_of_unitary, spectrum.subset_closedBall_norm, spectrum.vadd_eq, SpectrumRestricts.starAlgHom_id, IsometricContinuousFunctionalCalculus.isGreatest_spectrum, Module.End.HasUnifEigenvalue.mem_spectrum, continuousFunctionalCalculus_map_id, spectrum.sub_singleton_eq, IsCompactOperator.hasEigenvalue_iff_mem_spectrum, CStarAlgebra.nnnorm_mem_spectrum_of_nonneg, Unitary.spectrum_subset_circle, cfcHom_apply_mem_elemental, Matrix.posSemidef_iff_isHermitian_and_spectrum_nonneg, SpectrumRestricts.starAlgHom_injective, spectrum.notMem_iff, cfcUnits_zpow, isometry_cfcHom, CFC.spectrum_zero_eq, unitary.spectrum_subset_slitPlane_iff_norm_lt_two, Matrix.spectrum_toLin'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
resolventSet_neg 📖	mathematical	—	resolventSet CommRing.toCommSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Set Set.neg CommRing.toRing	—	Set.ext sub_neg_eq_add map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass

spectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_mem_add_iff 📖	mathematical	—	Set Set.instMembership spectrum Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap NonAssocSemiring.toNonUnitalNonAssocSemiring	—	add_mem_iff neg_add_cancel_left
add_mem_iff 📖	mathematical	—	Set Set.instMembership spectrum Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DFunLike.coe RingHom Ring.toSemiring RingHom.instFunLike algebraMap	—	map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass sub_neg_eq_add
add_singleton_eq 📖	mathematical	—	Set Set.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing spectrum CommRing.toCommSemiring Set.instSingletonSet NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap	—	singleton_add_eq add_comm
algebraMap_mem 📖	mathematical	Set Set.instMembership spectrum	Set Set.instMembership spectrum DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	algebraMap_mem_iff
algebraMap_mem_iff 📖	mathematical	—	Set Set.instMembership spectrum DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	Algebra.algebraMap_eq_smul_one smul_assoc one_smul
inv_mem_iff 📖	mathematical	—	Set Set.instMembership spectrum Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CommSemiring.toSemiring Units Units.instInv	—	not_iff_not inv_mem_resolventSet
inv_mem_resolventSet 📖	mathematical	Set Set.instMembership resolventSet Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CommSemiring.toSemiring	Set Set.instMembership resolventSet Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Units Units.instInv CommSemiring.toSemiring	—	mem_resolventSet_iff Algebra.algebraMap_eq_smul_one Units.smul_def IsUnit.smul_sub_iff_sub_inv_smul Units.instIsScalarTower IsScalarTower.right Units.smulCommClass_left Algebra.to_smulCommClass inv_inv IsUnit.sub_iff mul_sub mul_smul_comm Units.mul_inv mul_one sub_mul smul_mul_assoc Units.inv_mul one_mul Commute.isUnit_mul_iff
inv₀_mem 📖	mathematical	Set Set.instMembership spectrum Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Units Units.instInv	Set Set.instMembership spectrum Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	inv₀_mem_iff
inv₀_mem_iff 📖	mathematical	—	Set Set.instMembership spectrum Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Units Units.instInv	—	eq_or_ne inv_zero CanLift.prf instCanLiftUnitsValIsUnit Ne.isUnit inv_inv Units.val_inv_eq_inv_val
inv₀_mem_inv 📖	mathematical	Set Set.instMembership spectrum Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	Set Set.instMembership spectrum Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Units Units.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	inv₀_mem_inv_iff
inv₀_mem_inv_iff 📖	mathematical	—	Set Set.instMembership spectrum Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Units Units.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	inv_inv
isUnit_of_zero_notMem 📖	mathematical	Set Set.instMembership spectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	zero_notMem_iff
isUnit_resolvent 📖	mathematical	—	Set Set.instMembership resolventSet IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring resolvent	—	isUnit_ringInverse
map_inv 📖	mathematical	—	Set Set.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield spectrum Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Units Units.instInv	—	Set.ext
map_star 📖	mathematical	—	spectrum Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid Set Set.star	—	Set.ext star_mem_resolventSet_iff
mem_iff 📖	mathematical	—	Set Set.instMembership spectrum IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	—
mem_resolventSet_iff 📖	mathematical	—	Set Set.instMembership resolventSet IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	—
mem_resolventSet_of_left_right_inverse 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	Set Set.instMembership resolventSet	—	Units.isUnit left_inv_eq_right_inv
ne_zero_of_mem_of_unit 📖	—	Set Set.instMembership spectrum Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	—	zero_mem_resolventSet_of_unit
neg_eq 📖	mathematical	—	Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing spectrum CommRing.toCommSemiring	—	eq_1 Set.compl_neg resolventSet_neg
nonzero_mul_comm 📖	mathematical	—	Set Set.instSDiff spectrum Semifield.toCommSemiring Field.toSemifield Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Set.instSingletonSet MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	unit_mem_mul_comm Set.eq_of_subset_of_subset
notMem_iff 📖	mathematical	—	Set Set.instMembership spectrum IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	—
not_isUnit_of_zero_mem 📖	mathematical	Set Set.instMembership spectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	zero_mem_iff
of_algebraMap_mem 📖	mathematical	Set Set.instMembership spectrum DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	Set Set.instMembership spectrum	—	algebraMap_mem_iff
of_inv₀_mem 📖	mathematical	Set Set.instMembership spectrum Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	Set Set.instMembership spectrum Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Units Units.instInv	—	inv₀_mem_iff
of_inv₀_mem_inv 📖	mathematical	Set Set.instMembership spectrum Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Units Units.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	Set Set.instMembership spectrum Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	inv₀_mem_inv_iff
of_subsingleton 📖	mathematical	—	spectrum Set Set.instEmptyCollection	—	eq_1 resolventSet_of_subsingleton Set.compl_univ
one_eq 📖	mathematical	—	spectrum Semifield.toCommSemiring Field.toSemifield AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Set Set.instSingletonSet DivisionRing.toRing Field.toDivisionRing	—	Algebra.algebraMap_eq_smul_one one_smul scalar_eq
preimage_algebraMap 📖	mathematical	—	Set.preimage DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap spectrum	—	Set.ext algebraMap_mem_iff
preimage_units_mul_comm 📖	mathematical	—	Set.preimage Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Units.val spectrum Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Set.ext unit_mem_mul_comm
resolventSet_of_subsingleton 📖	mathematical	—	resolventSet Set.univ	—	—
resolvent_eq 📖	mathematical	Set Set.instMembership resolventSet	resolvent Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Units Units.instInv IsUnit.unit SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	Ring.inverse_unit
scalar_eq 📖	mathematical	—	spectrum Semifield.toCommSemiring Field.toSemifield DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap Set Set.instSingletonSet	—	add_zero singleton_add_eq zero_eq Set.singleton_add_singleton
setOf_isUnit_inter_mul_comm 📖	mathematical	—	Set Set.instInter setOf IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring spectrum Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Set.ext unit_mem_mul_comm
singleton_add_eq 📖	mathematical	—	Set Set.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Set.instSingletonSet spectrum CommRing.toCommSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap	—	Set.ext Set.singleton_add Set.image_add_left Set.mem_preimage add_comm add_mem_iff map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass neg_neg
singleton_sub_eq 📖	mathematical	—	Set Set.sub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Set.instSingletonSet spectrum CommRing.toCommSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap	—	sub_eq_add_neg neg_eq singleton_add_eq
smul_eq_smul 📖	mathematical	Set.Nonempty spectrum Semifield.toCommSemiring Field.toSemifield	spectrum Semifield.toCommSemiring Field.toSemifield Algebra.toSMul Ring.toSemiring Set Set.smulSet CommSemiring.toSemiring Algebra.id	—	eq_or_ne zero_smul zero_eq Set.zero_smul_set unit_smul_eq_smul
smul_mem_smul_iff 📖	mathematical	—	Set Set.instMembership spectrum Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Units.instSMul Algebra.toSMul Ring.toSemiring Algebra.id	—	Algebra.algebraMap_eq_smul_one smul_assoc Units.instIsScalarTower IsScalarTower.left Units.smulCommClass_left Algebra.to_smulCommClass IsScalarTower.right
star_mem_resolventSet_iff 📖	mathematical	—	Set Set.instMembership resolventSet Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid	—	Algebra.algebraMap_eq_smul_one star_sub StarModule.star_smul star_star star_one IsUnit.star
sub_singleton_eq 📖	mathematical	—	Set Set.sub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing spectrum CommRing.toCommSemiring Set.instSingletonSet DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap	—	neg_sub neg_eq singleton_sub_eq
subset_singleton_zero_compl 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	Set Set.instHasSubset spectrum Compl.compl Set.instCompl Set.instSingletonSet MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Set.subset_compl_singleton_iff zero_notMem
subset_subalgebra 📖	mathematical	—	Set Set.instHasSubset spectrum SetLike.instMembership SubringClass.toRing SubalgebraClass.toAlgebra Ring.toSemiring	—	Set.compl_subset_compl IsUnit.map SubringClass.toSubsemiringClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
unit_mem_mul_comm 📖	mathematical	—	Set Set.instMembership spectrum Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring	—	sub_eq_add_neg IsUnit.unit.congr_simp mul_assoc mul_add Distrib.leftDistribClass mul_one add_mul Distrib.rightDistribClass one_mul neg_mul mul_neg IsUnit.mul_val_inv sub_add_cancel Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.const_add_termg IsUnit.val_inv_mul Algebra.algebraMap_eq_smul_one Units.instIsScalarTower IsScalarTower.right Units.smulCommClass_left Algebra.to_smulCommClass smul_mul_assoc mul_smul_comm
unit_smul_eq_smul 📖	mathematical	—	spectrum Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Units.instSMul Algebra.toSMul Ring.toSemiring Set Set.smulSet Algebra.id	—	Set.ext smul_inv_smul smul_mem_smul_iff inv_smul_smul
units_conjugate 📖	mathematical	—	spectrum Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Units Units.instInv	—	mem_iff Mathlib.Tactic.Contrapose.contrapose₄ mul_sub sub_mul Algebra.right_comm Units.mul_inv one_mul IsUnit.mul Units.isUnit le_antisymm mul_assoc Units.inv_mul_cancel_left inv_inv Units.inv_mul mul_one
units_conjugate' 📖	mathematical	—	spectrum Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Units Units.instInv	—	inv_inv units_conjugate
units_smul_resolvent 📖	mathematical	—	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Units.instSMul Algebra.toSMul Ring.toSemiring resolvent Units.instInv Algebra.id	—	Algebra.algebraMap_eq_smul_one smul_assoc Units.instIsScalarTower IsScalarTower.left smul_sub mem_iff smul_inv_smul IsUnit.smul Units.smulCommClass_left Algebra.to_smulCommClass IsScalarTower.right Ring.inverse_non_unit smul_zero notMem_iff IsUnit.val_subInvSMul IsUnit.unit_spec Ring.inverse_unit IsUnit.val_inv_subInvSMul IsUnit.unit.congr_simp
units_smul_resolvent_self 📖	mathematical	—	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Units.instSMul Algebra.toSMul Ring.toSemiring resolvent Units.val Units.instInv AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	Units.inv_mul units_smul_resolvent
vadd_eq 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing AddAction.toAddSemigroupAction AddMonoid.toAddAction spectrum CommRing.toCommSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap	—	Set.singleton_add singleton_add_eq
zero_eq 📖	mathematical	—	spectrum Semifield.toCommSemiring Field.toSemifield MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Set Set.instSingletonSet NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	Set.Subset.antisymm eq_1 Set.compl_subset_comm Set.mem_compl_singleton_iff IsUnit.smul Units.smulCommClass_left Algebra.to_smulCommClass Units.instIsScalarTower IsScalarTower.right isUnit_one Algebra.algebraMap_eq_smul_one sub_zero zero_smul sub_self NeZero.one
zero_mem 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	Set Set.instMembership spectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	zero_mem_iff
zero_mem_iff 📖	mathematical	—	Set Set.instMembership spectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	mem_iff map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass zero_sub IsUnit.neg_iff
zero_mem_resolventSet_of_unit 📖	mathematical	—	Set Set.instMembership resolventSet Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Units.isUnit
zero_notMem 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	Set Set.instMembership spectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	zero_notMem_iff
zero_notMem_iff 📖	mathematical	—	Set Set.instMembership spectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	zero_mem_iff

---

← Back to Index