leanprover-community/mathlib3

Pull Requests Commits

feat(category_theory/nat_iso): add simp lemmas (#13303)

kim-em committed 4 years ago

722c0dfa

feat(analysis/special_functions/pow): `z ^ w` is continuous in `(z, w)` at `(0, w)` if `0 < re w` (#13288)

urkud committed 4 years ago

f7e862f6

feat(data/complex/is_R_or_C): add `polynomial.of_real_eval` (#13287)

urkud committed 4 years ago

57682ffa

feat(analysis/asymptotics): add a few versions of `c=o(x)` as `x→∞` (#13286)

urkud committed 4 years ago

577df07c

feat(group_theory/group_action/basic): A `quotient_action` induces an action on left cosets (#13283)

tb65536 committed 4 years ago

171e2aa2

feat(group_theory/transversal): A `quotient_action` induces an action on left transversals (#13282)

tb65536 committed 4 years ago

65b5dd8b

chore(topology/algebra/uniform_group): use morphism classes (#13273)

ADedecker committed 4 years ago

2eba5241

feat(topology/order): if `e` is an equiv, `induced e.symm = coinduced e` (#13272)

ADedecker committed 4 years ago

2b80d4a0

feat(algebra/big_operators): `norm_num` plugin for list/multiset/finset prod/sum (#13005)

Vierkantor committed 4 years ago

c1600832

feat(scripts): make style lint script more robust to lines starting with spaces (#13317)

alexjbest committed 4 years ago

e5bd9413

feat(analysis/special_functions/pow): more versions of `x ^ k = o(exp(b * x))` (#13285)

urkud committed 4 years ago

cd616e0d

fix(algebra/indicator_function): fix name of `mul_indicator_eq_one_iff` (#13284)

urkud committed 4 years ago

706905c5

feat(model_theory/basic): Structures over the empty language (#13281)

awainverse committed 4 years ago

ff507a35

feat(topology/algebra/uniform_group): a subgroup of a uniform group is a uniform group (#13277)

ADedecker committed 4 years ago

fe17fee1

feat(group_theory/schreier): Finset version of Schreier's lemma (#13274)

tb65536 committed 4 years ago

6f428ed4

fix(algebra/module/basic,group_theory/group_action/defs): generalize nat and int smul_comm_class instances (#13174)

eric-wieser committed 4 years ago

102311e6

refactor(order/conditionally_complete_lattice): `csupr_le_csupr` → `csupr_mono` (#13320)

vihdzp committed 4 years ago

4d27ecf7

chore(*): make more transitive relations available to calc (#12860)

ericrbg committed 4 years ago

6f9cb03e

chore(measure_theory/mconstructions/prod): Speed up `finite_spanning_sets_in.prod` (#13325)

YaelDillies committed 4 years ago

a85958cf

feat(topology/algebra/order): add `le_on_closure` (#13290)

urkud committed 4 years ago

a2d09b24

chore(topology/uniform_space/basic): golf a proof (#13289)

urkud committed 4 years ago

e5ae0991

chore(algebra/invertible): generalise typeclasses (#13275)

ericrbg committed 4 years ago

84910217

fix(field_theory/galois): update docstring (#13188)

kbuzzard committed 4 years ago

4ded5ca3

feat(data/sym/basic): some basic lemmas in preparation for stars and bars (#12479)

stuart-presnell committed 4 years ago

be22d07e

feat(set_theory/cofinality): Every ordinal has a fundamental sequence (#12317)

vihdzp committed 4 years ago

609eb59e

chore(category_theory/fin_category): Speed up `as_type_equiv_obj_as_type` (#13298)

YaelDillies committed 4 years ago

5bf57407

feat(linear_algebra): add `adjoint_pair` from `bilinear_form` (#13203)

mcdoll committed 4 years ago

60ccf8f7

feat(set_theory/cardinal_ordinal): Simp lemmas for `mk` (#13119)

vihdzp committed 4 years ago

a30cba49

feat(category_theory/monoidal): coherence tactic (#13125)

kim-em committed 4 years ago

965f46d4

feat(data/fin/tuple/nat_antidiagonal): add `antidiagonal_tuple` (#13031)

eric-wieser committed 4 years ago

0bc2aa91

Newer Older