leanprover-community/mathlib

Pull Requests Commits

TwoFX committed 4 years ago

98a76b8f

chore(dynamics/periodic_pts): remove duplicate of nat.dvd_right_iff_eq (#7435)

Ruben-VandeVelde committed 4 years ago

58e990d9

feat(topology/category/Profinite): Any continuous bijection of profinite spaces is an isomorphism. (#7430)

adamtopaz committed 4 years ago

4bd1c836

feat(topology/discrete_quotient): Discrete quotients of topological spaces (#7425)

adamtopaz committed 4 years ago

30f3788c

feat(linear_algebra/char_poly): charpoly of `left_mul_matrix` (#7397)

Vierkantor committed 4 years ago

6d7e7563

feat(field_theory/polynomial_galois_group): Galois group is S_p (#7352)

tb65536 committed 4 years ago

cfc74155

feat(category_theory/limits): dualizing some results (#7391)

kim-em committed 4 years ago

6624bbe7

feat(group_theory/perm/{cycles, cycle_type}): permutations are conjugate iff they have the same cycle type (#7335)

awainverse committed 4 years ago

6e836c43

feat(category_theory): definition of R-linear category (#7321)

kim-em committed 4 years ago

106ac8e0

feat(geometry/euclidean/basic): lemmas about angles and distances (#7140)

manuelcandales committed 4 years ago

decb556e

feat(topology/continuous_function): the Stone-Weierstrass theorem (#7305)

kim-em committed 4 years ago

ea379b09

feat(category_theory/monoidal): the monoidal coherence theorem (#7324)

TwoFX committed 4 years ago

d3c565d4

feat(algebra/archimedean): rat.cast_round for non-archimedean fields (#7424)

gebner committed 4 years ago

790ec6b1

chore(topology/continuous_function/algebra): put `coe_fn_monoid_hom `into the `continuous_map` namespace (#7423)

eric-wieser committed 4 years ago

92b90480

chore(measure_theory/ae_eq_fun_metric): remove useless file (#7419)

sgouezel committed 4 years ago

55112757

feat(linear_algebra/quadratic_form): add lemmas about sums of quadratic forms (#7417)

eric-wieser committed 4 years ago

d04af204

chore(algebra/algebra/basic): add missing lemmas (#7412)

eric-wieser committed 4 years ago

bf0f15ab

fix(algebra/direct_sum_graded): replace badly-stated and slow `simps` lemmas with manual ones (#7403)

eric-wieser committed 4 years ago

e3de4e30

feat(analysis/special_functions/integrals): integral of `cos x ^ n` (#7402)

benjamindavidson committed 4 years ago

aa37eeea

feat(algebra/polynomial): generalize to `multiset` products (#7399)

Vierkantor committed 4 years ago

2cc8128f

feat(algebra/squarefree): add sq_mul_squarefree lemmas (#7282)

manuelcandales committed 4 years ago

d5d22c5d

feat(data/polynomial/coeff): Add smul_eq_C_mul (#7240)

BoltonBailey committed 4 years ago

b51cee2b

feat(category_theory/enriched): abstract enriched categories (#7175)

kim-em committed 4 years ago

b88a9d14

feat(linear_algebra/determinant): various operations preserve the determinant (#7115)

Vierkantor committed 4 years ago

802c5b5a

refactor(group_theory/order_of_element): use minimal_period for the definition (#7082)

Julian-Kuelshammer committed 4 years ago

6c617793

feat(algebraic_geometry/prime_spectrum): Basic opens are compact (#7411)

justus-springer committed 4 years ago

16c8f7f3

refactor(algebra/group_power): put lemmas about order and power in their own file (#7398)

eric-wieser committed 4 years ago

aebe7552

refactor(linear_algebra/eigenspace): cleanup proof (#7337)

kim-em committed 4 years ago

6d5a120f

feat(category_theory/Quiv): the free/forgetful adjunction between Cat and Quiv (#7158)

kim-em committed 4 years ago

5800f69a

feat(category_theory/sites): construct a presieve from an indexed family of arrows (#7413)

b-mehta committed 4 years ago

64fdfc74

Older