leanprover-community/mathlib3

Pull Requests Commits

add endofunctor.algebra (#12642)

Jlh18 committed 3 years ago

f8d947c7

refactor(set_theory/ordinal_arithmetic): Turn various results into simp lemmas (#12661)

vihdzp committed 3 years ago

174f1da1

docs(algebra/*): Add docstrings to additive lemmas (#12578)

YaelDillies committed 3 years ago

ad0988b3

feat(analysis/inner_product_space/pi_L2): `linear_isometry.extend` (#12192)

hparshall committed 3 years ago

580e1d95

feat(measure_theory/group/fundamental_domain): ess_sup_measure_restrict (#12603)

AlexKontorovich committed 3 years ago

3751ec63

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

Newer Older