leanprover-community/mathlib

Pull Requests Commits

fixed to/of issues

antoinelab01 committed 3 years ago

7f538f67

fixed types in tensor_rep_def

antoinelab01 committed 3 years ago

aa664466

antoinelab01 committed 3 years ago

17bf7cd2

Merge branch 'hom_rep' of https://github.com/leanprover-community/mathlib into hom_rep

antoinelab01 committed 3 years ago

d8995008

antoinelab01 committed 3 years ago

6bd69092

Update src/representation_theory/basic.lean

antoinelab01 committed 3 years ago

Verified b78ad4ad

antoinelab01 committed 3 years ago

20abb242

feat(representation_theory/basic): add a few constructions of group representations

antoinelab01 committed 3 years ago

b2c0cb36

feat(group_theory/subgroup/basic): One more `mem_normalizer_iff` lemma (#13395)

tb65536 committed 3 years ago

251bd842

feat(combinatorics/additive/salem_spencer): Salem-Spencer sets under images (#13279)

YaelDillies committed 3 years ago

8bbc5ac4

feat(measure_theory/card_measurable_space): `generate_measurable_rec s` gives precisely the generated sigma-algebra (#12462)

vihdzp committed 3 years ago

fecdd4b2

feat(topology/algebra/order/compact): Sup is continuous (#13347)

fpvandoorn committed 3 years ago

adfe9c7f

feat(analysis/normed_space/finite_dimension): a finite dimensional affine subspace is closed (#13440)

urkud committed 3 years ago

936eb7ee

feat(ring_theory/multiplicity): int.nat_abs (#13420)

BoltonBailey committed 3 years ago

9631a913

feat(measure_theory/constructions/pi): more `measure_preserving` lemmas (#13404)

urkud committed 3 years ago

88ba31c9

refactor(group_theory/schur_zassenhaus): Golf using `is_complement'_stabilizer` (#13392)

tb65536 committed 3 years ago

dd34ffaf

feat(group_theory/complement): Add more API for the action on left transversals (#13363)

tb65536 committed 3 years ago

15b764d8

feat(group_theory/group_action/basic): Right multiplication satisfies the `quotient_action` axiom (#13362)

tb65536 committed 3 years ago

769ec8c8

chore(order/complete_lattice): General cleanup (#13323)

vihdzp committed 3 years ago

3676f11d

feat(category_theory): turn a split mono with cokernel into a biproduct (#13184)

javra committed 3 years ago

7bb10813

feat(number_theory/legendre_symbol): add directory legendre_symbol and move quadratic_reciprocity.lean into it (#13441)

MichaelStollBayreuth committed 3 years ago

2693ab58

feat(topology/unit_interval): add lemmas (#13344)

fpvandoorn committed 3 years ago

eb2780b6

chore(data/nat/factorial): tidy (#13436)

ericrbg committed 3 years ago

87f8076f

feat(data/mv_polynomial): add support_X_pow (#13435)

alexjbest committed 3 years ago

dac4f18f

feat(complex/roots_of_unity): extensionality (#13431)

ericrbg committed 3 years ago

1378eabf

chore(*): suggestions from the generalisation linter (#13092)

kim-em committed 3 years ago

2249a240

chore(scripts): update nolints.txt (#13438)

leanprover-community-bot committed 3 years ago

a5654710

feat(complex/arg): arg_eq_zero_iff (#13432)

ericrbg committed 3 years ago

b62626e5

chore(order/category/Preorder): reduce imports (#13301)

kim-em committed 3 years ago

0765994d

feat(data/polynomial/*): suggestions from the generalization linter (#13342)

kim-em committed 3 years ago

6f401acf

Older