leanprover-community/mathlib3

Pull Requests Commits

feat(analysis/*/{exponential, spectrum}): spectrum of a selfadjoint element is real (#12417)

j-loreaux committed 3 years ago

223e7428

chore(algebra/algebra/subalgebra): reduce imports (#12636)

kim-em committed 3 years ago

7d34f786

feat(analysis/normed_space/star/basic): `matrix.entrywise_sup_norm_star_eq_norm` (#12201)

hparshall committed 3 years ago

daa257ff

feat(algebra/algebra/spectrum): prove spectral inclusion for algebra homomorphisms (#12573)

j-loreaux committed 3 years ago

73530b52

feat(ring_theory/graded_algebra/homogeneous_ideal): definition of irrelevant ideal of a graded algebra (#12548)

jjaassoonn committed 3 years ago

9f1f8c13

feat(data/list/basic): Stronger form of `fold_fixed` (#12613)

vihdzp committed 3 years ago

5b369417

refactor(group_theory/commutator): Use variables and rearrange lemmas (#12629)

tb65536 committed 3 years ago

3da03b97

feat(category_theory/preadditive/Mat): ring version (#12617)

kim-em committed 3 years ago

23269bf0

feat(model_theory/definability): Definability with parameters (#12611)

awainverse committed 3 years ago

707df2cd

feat(algebra/category/Module): monoidal_preadditive (#12607)

kim-em committed 3 years ago

9293174a

feat(topology/algebra/continuous_monoid_hom): Define the Pontryagin dual (#12602)

tb65536 committed 3 years ago

e4ea2bca

feat(topology/category/Locale): The category of locales (#12580)

YaelDillies committed 3 years ago

5a9fb92b

feat(order/complete_lattice): add `complete_lattice.independent_pair` (#12565)

eric-wieser committed 3 years ago

96bae07c

chore(analysis/convex/strict): Reduce typeclass assumptions, golf (#12627)

YaelDillies committed 3 years ago

7e5ac6ad

feat(order/upper_lower): Upper/lower sets (#12189)

YaelDillies committed 3 years ago

22bdc8ec

chore(analysis): move lemmas around (#12621)

urkud committed 3 years ago

dc4e5cb4

chore(data/nat/prime): restate card_multiples without finset.sep (#12625)

Ruben-VandeVelde committed 3 years ago

7257ee71

chore(category_theory/closed/monoidal): fix notation (#12612)

kim-em committed 3 years ago

a63b99c3

chore(category_theory/limits): correct lemma names (#12606)

kim-em committed 3 years ago

956f3dbc

feat(group_theory/commutator): Prove `commutator_eq_bot_iff_le_centralizer` (#12598)

tb65536 committed 3 years ago

9456a744

feat(group_theory/subgroup/basic): add eq_one_of_noncomm_prod_eq_one_of_independent (#12525)

nomeata committed 3 years ago

b9ab27bd

split(analysis/locally_convex/basic): Split off `analysis.seminorm` (#12624)

YaelDillies committed 3 years ago

b21c1c9b

chore(algebra/category/Module): remove unnecessary universe restriction (#12610)

kim-em committed 3 years ago

a4187fef

fix(src/algebra/big_operators/multiset): unify prod_le_pow_card and prod_le_of_forall_le (#12589)

nomeata committed 3 years ago

31d28c62

feat(topology/homotopy): Homotopic maps induce naturally isomorphic functors between fundamental groupoid (#11595)

prakol16 committed 3 years ago

2241588b

doc(category_theory/monoidal/rigid): noting future work (#12620)

kim-em committed 3 years ago

5f3f70fe

refactor(group_theory/commutator): Golf proof of `commutator_mono` (#12619)

tb65536 committed 3 years ago

3d41a5bd

refactor(set_theory/ordinal_arithmetic): remove dot notation (#12614)

vihdzp committed 3 years ago

72c6979b

refactor(group_theory/commutator): Golf proof of `commutator_comm` (#12600)

tb65536 committed 3 years ago

3aaa5647

fix(tactic/suggest): fixing `library_search` (#12616)

arthurpaulino committed 3 years ago

1463f592

Newer Older