leanprover-community/mathlib3

Pull Requests Commits

refactor(set_theory/cardinal_ordinal): `aleph_is_principal_aleph` → `principal_add_aleph` (#12663)

vihdzp committed 3 years ago

7b7fea55

feat(set_theory/ordinal): `ord 1 = 1` (#12662)

vihdzp committed 3 years ago

6ebb3786

feat(algebra/support) support of power is subset of support (#12654)

Multramate committed 3 years ago

18ba3950

chore(topology/algebra/group_with_zero): fix docstring for has_continuous_inv0 (#12653)

sgouezel committed 3 years ago

6b3b567f

feat(analysis/seminorm): add lemmas for `with_seminorms` (#12649)

mcdoll committed 3 years ago

1f5950a7

move(topology/sets/*): Move topological types of sets together (#12648)

YaelDillies committed 3 years ago

b6fa3beb

chore(analysis/locally_convex/basic): generalize lemmas and add simple lemmas (#12643)

mcdoll committed 3 years ago

778dfd50

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

Newer Older