Commit 2023-06-07 16:52 4d53e9ff

View on Github →

feat: port Algebra.Algebra.Spectrum (#4778)

depends on: #4804

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Algebra/Spectrum.lean

added theorem AlgHom.apply_mem_spectrum

added theorem AlgHom.mem_resolventSet_apply

added theorem AlgHom.spectrum_apply_subset

added def resolventSet

added theorem spectrum.add_mem_add_iff

added theorem spectrum.add_mem_iff

added theorem spectrum.add_singleton_eq

added theorem spectrum.inv_mem_iff

added theorem spectrum.inv_mem_resolventSet

added theorem spectrum.isUnit_resolvent

added theorem spectrum.mem_iff

added theorem spectrum.mem_resolventSet_iff

added theorem spectrum.mem_resolventSet_of_left_right_inverse

added theorem spectrum.ne_zero_of_mem_of_unit

added theorem spectrum.neg_eq

added theorem spectrum.nonzero_mul_eq_swap_mul

added theorem spectrum.not_mem_iff

added theorem spectrum.of_subsingleton

added theorem spectrum.one_eq

added theorem spectrum.preimage_units_mul_eq_swap_mul

added theorem spectrum.resolventSet_of_subsingleton

added theorem spectrum.resolvent_eq

added theorem spectrum.scalar_eq

added theorem spectrum.singleton_add_eq

added theorem spectrum.singleton_sub_eq

added theorem spectrum.smul_eq_smul

added theorem spectrum.smul_mem_smul_iff

added theorem spectrum.star_mem_resolventSet_iff

added theorem spectrum.sub_singleton_eq

added theorem spectrum.subset_starSubalgebra

added theorem spectrum.subset_subalgebra

added theorem spectrum.unit_mem_mul_iff_mem_swap_mul

added theorem spectrum.unit_smul_eq_smul

added theorem spectrum.units_smul_resolvent

added theorem spectrum.units_smul_resolvent_self

added theorem spectrum.vadd_eq

added theorem spectrum.zero_eq

added theorem spectrum.zero_mem_iff

added theorem spectrum.zero_mem_resolventSet_of_unit

added theorem spectrum.zero_not_mem_iff

added def spectrum