leanprover-community/mathlib

Pull Requests Commits

urkud committed 3 years ago

23c57639

urkud committed 3 years ago

8b102e6b

Merge branch 'master' into YK-fintype-finite

urkud committed 3 years ago

fdafe569

feat(analysis/calculus/cont_diff): generalize `mul` lemmas to a normed algebra (#15595)

urkud committed 3 years ago

d98479aa

doc(number_theory/bernoulli_polynomials): a few small improvements (#15599)

alexjbest committed 3 years ago

91416440

feat(order/succ_pred/limit): Successor and predecessor limits (#15001)

vihdzp committed 3 years ago

767aeb39

feat(order/initial_seg): Initial/principal segment from empty type (#15375)

vihdzp committed 3 years ago

9bf23b0a

feat(data/real/basic): add a repr showing an underlying cauchy sequence (#15575)

eric-wieser committed 3 years ago

d749b205

feat(linear_algebra/linear_pmap): more lemmas about the graph (#15531)

mcdoll committed 3 years ago

c0c910de

chore(data/real/basic,number_theory/padics/padic_numbers): eliminate `real.of_rat` and `padic.of_rat` (#15569)

eric-wieser committed 3 years ago

591992d7

feat(topology/partition_of_unity): local to global (#15490)

urkud committed 3 years ago

7f16dd20

refactor(set_theory/zfc): make `Class` morally `Set → Prop` (#15248)

vihdzp committed 3 years ago

f05fdcac

feat(set_theory/cardinal/ordinal): basic properties on Beth numbers (#14989)

vihdzp committed 3 years ago

99625b1b

feat(algebraic_topology/dold_kan): technical lemmas about face maps (#14044)

joelriou committed 3 years ago

d29aca84

doc(data/dfinsupp): improve the docstring for dfinsupp (#15554)

eric-wieser committed 3 years ago

72e0e9a5

feat(set_theory/zfc/ordinal): more lemmas on transitive sets (#15548)

vihdzp committed 3 years ago

8672734e

fix(data/set_like): `coe_sort_trans` should have low priority (#15489)

Vierkantor committed 3 years ago

8983bec7

refactor(field_theory/*): Refactor `normal` to use `is_algebraic` (#15421)

tb65536 committed 3 years ago

62b5bb74

feat(linear_algebra/projective_space/subspace): defines subspaces of a projective space (#15391)

Michael14071407 committed 3 years ago

90a44f6b

feat(ring_theory/graded_algebra/basic): add lemma `proj_homogeneous_mul` (#15264)

jjaassoonn committed 3 years ago

976f5106

feat(topology/basic): a condition implying that a sequence of functions locally stabilizes (#15580)

urkud committed 3 years ago

4a09c733

feat(logic/nonempty): `pi.nonempty` instance (#15574)

vihdzp committed 3 years ago

6b5a1730

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

leanprover-community-bot committed 3 years ago

b5e9ffd2

feat(analysis/normed_space/operator_norm): variant of `continuous_linear_equiv.has_sum` (#15578)

ADedecker committed 3 years ago

6b34a400

feat(analysis/inner_product_space/basic): `orthonormal` version of `linear_independent.coe_range` (#15577)

ADedecker committed 3 years ago

8ab47c53

feat(combinatorics/simple_graph/connectivity): operations and lemmas about path type (#15156)

kmill committed 3 years ago

eece0d9b

feat(group_theory/subsemigroup/membership): add membership criteria for subsemigroups (#13945)

j-loreaux committed 3 years ago

3ce710a7

chore(tactic/*): clean up doc tags (#15563)

robertylewis committed 3 years ago

e1eba9fa

chore(algebra/module/injective): golf some proofs (#15534)

Ruben-VandeVelde committed 3 years ago

9696524a

feat(analysis/normed_space/linear_isometry): `linear_equiv.of_eq` as a `linear_isometry_equiv` (#15471)

ADedecker committed 3 years ago

34d4a9bf

Older