leanprover-community/mathlib3

Pull Requests Commits

feat(analysis/normed_space/operator_norm): add 2 new versions of `op_norm_le_*` (#15417)

urkud committed 3 years ago

65a44e6f

doc(set_theory/game/nim): update module docs (#15406)

vihdzp committed 3 years ago

86597b31

feat(order/initial_seg): remove `nolint` from `initial_seg` (#15374)

vihdzp committed 3 years ago

d3051b17

feat(algebra/order/monoid): add lemmas `map_add` for `with_bot/top` (#15300)

adomani committed 3 years ago

f73befff

refactor(data/real/ennreal): redefine `ennreal.to_nnreal` in terms of `with_top.untop'` (#15247)

urkud committed 3 years ago

101555b1

feat(data/finsupp/big_operators): sum of finsupp and their support (#15155)

pechersky committed 3 years ago

93fbab6d

chore({algebra,data/rat}): use forgetful inheritance for `algebra_rat` (#14894)

Vierkantor committed 3 years ago

2ee2bae0

feat(algebraic_topology): alternating_coface_map_complex (#14588)

joelriou committed 3 years ago

5797ef5c

Merge branch 'is_succ_limit' into is_succ_limit_pred'

vihdzp committed 3 years ago

2b941413

feat(data/polynomial/degree/lemmas): three lemmas on nat_degrees, bits and neg (#15522)

adomani committed 3 years ago

48c6cc31

feat(field_theory/adjoin): `intermediate_field.exists_finset_of_mem_supr` (#15518)

tb65536 committed 3 years ago

35639363

chore(order/upper_lower): fix typo (#15517)

vihdzp committed 3 years ago

c55cadbc

chore(set_theory/game/nim): reorder lemmas (#15516)

vihdzp committed 3 years ago

d6655353

chore(logic/equiv): improve defeq and/or simp lemmas about some equivs (#15511)

urkud committed 3 years ago

fd7796a1

feat(data/pnat/basic): add lemmas, move `equiv.pnat_equiv_nat` (#15508)

urkud committed 3 years ago

72eaefff

feat(analysis/special_functions/exp): add lemmas about `is_o`/`is_O`/`is_Theta` (#15506)

urkud committed 3 years ago

8f000ca2

feat(tactic/ext): don't remove attr (#15502)

alexjbest committed 3 years ago

b2af6ee9

refactor(algebra/graded_monoid): provide better names for lemmas about internal graduations (#15488)

eric-wieser committed 3 years ago

461afdac

feat(number_theory): degree `[Frac(S):Frac(R)]` is degree `[S/pS:R/p]` (#15315)

Vierkantor committed 3 years ago

93219fb7

feat(ring_theory/etale): Formally étale morphisms. (#15242)

erdOne committed 3 years ago

1b775c2c

refactor(group_theory/group_action/basic): Make `mul_action.self_equiv_sigma_orbits` computable (#14591)

eric-wieser committed 3 years ago

3527e4ad

feat(representation_theory/Action): mapping by a monoidal functor (#14331)

kim-em committed 3 years ago

1e72fb3f

feat(set_theory/zfc): `Ø ⊆ x` (#15223)

vihdzp committed 3 years ago

c70a787e

feat(topology/support): add lemmas, fix a name (#15484)

urkud committed 3 years ago

e1c8bded

feat(field_theory/adjoin): Compact elements of `intermediate_field` (#15438)

tb65536 committed 3 years ago

ebe60290

feat(analysis/calculus): generalize `differentiable*.pow`, add `differentiable*.zpow` (#15416)

urkud committed 3 years ago

150b8e81

feat(analysis/inner_product/calculus): [higher] differentiability to/from `euclidean_space` (#15363)

ADedecker committed 3 years ago

632b4970

refactor(set_theory/zfc): `Union` → `sUnion` (#15352)

vihdzp committed 3 years ago

58d7431d

feat(set_theory/zfc): `∈` is well-founded (#15213)

vihdzp committed 3 years ago

11576dbb

feat(topology/algebra/filter_basis): add a variant of `module_filter_basis.has_continuous_smul` when we already have a topological group (#14806)

ADedecker committed 3 years ago

d655f459

Newer Older