leanprover-community/mathlib3

Pull Requests Commits

feat(algebra/lie/tensor_product): prove `lie_submodule.lie_ideal_oper_eq_tensor_map_range` (#7313)

ocfnash committed 4 years ago

5ac79a63

feat(group_theory/finiteness): add submonoid.fg (#7279)

riccardobrasca committed 4 years ago

35b9d9c4

feat(topology/unit_interval): affine homeomorphisms of intervals (#7250)

kim-em committed 4 years ago

5258669e

chore(algebra/lie/nilpotent): make proof of `module.derived_series_le_lower_central_series` less refl-heavy (#7359)

ocfnash committed 4 years ago

c22de3f5

feat(data/nat/fib): add a strict monotonicity lemma. (#7317)

Julian committed 4 years ago

95260613

chore(analysis/special_functions/integrals): reorganize file (#7351)

benjamindavidson committed 4 years ago

4e0c460a

feat(data/matrix/basic): transform vec_mul to mul_vec (#7348)

gabrielmoise committed 4 years ago

dbc9cf9f

chore(ring_theory/ideal/operations): golf and remove @ (#7347)

eric-wieser committed 4 years ago

d5cb4033

feat(ring_theory): fg_iff_exists_fin_generating_fam (#7343)

PatrickMassot committed 4 years ago

3821d318

feat(linear_algebra): free_of_finite_type_torsion_free (#7341)

PatrickMassot committed 4 years ago

9cc3d80e

refactor(*): kill int multiplication diamonds (#7255)

sgouezel committed 4 years ago

8e4ef23a

feat(order/extension): extend partial order to linear order (#7142)

b-mehta committed 4 years ago

d052c527

chore(algebra/category): remove duplicated proofs (#7349)

TwoFX committed 4 years ago

d5330fe8

feat(data/finsupp): to_multiset symm apply (#7356)

b-mehta committed 4 years ago

6b2bb8a1

feat(data/list/basic): assorted list lemmas (#7296)

pechersky committed 4 years ago

beb694b9

feat(data/list/forall2): defines sublist_forall2 relation (#7165)

awainverse committed 4 years ago

77168704

feat(archive/imo): IMO 2001 Q2 (#7238)

peakpoint committed 4 years ago

2ecd65e6

feat(linear_algebra): Lagrange formulas for expanding `det` along a row or column (#6897)

Vierkantor committed 4 years ago

8f8b194a

feat(group_theory/nielsen_schreier): subgroup of free group is free (#6840)

dwarn committed 4 years ago

f83ae595

refactor(*): rename `semimodule` to `module`, delete typeclasses `module` and `vector_space` (#7322)

Vierkantor committed 4 years ago

46ceb36e

chore(docs/100.yaml): mention "Erdős–Szekeres" by name (#7353)

benjamindavidson committed 4 years ago

f15887a1

feat(data/int/basic): add nat_abs_ne_zero (#7350)

Ruben-VandeVelde committed 4 years ago

767c8c59

feat(group_theory/{perm/cycle_type, specific_groups/alternating_group}): the alternating group is generated by 3-cycles (#6949)

awainverse committed 4 years ago

27cd5c11

feat(topology/algebra): uniform continuity from 0 (#7318)

b-mehta committed 4 years ago

bbd9362d

refactor(field_theory/algebraic_closure): move complex.is_alg_closed (#7344)

kim-em committed 4 years ago

d89f93a9

feat(algebra/star/pi): star operates elementwise on pi types (#7342)

eric-wieser committed 4 years ago

bb2e7f9e

chore(algebra/opposite): add missing `monoid_with_zero` instance (#7339)

eric-wieser committed 4 years ago

a5b5f6c3

feat(analysis/specific_limits): basic ratio test for summability of a nat-indexed family (#7277)

ADedecker committed 4 years ago

6c092955

feat(linear_algebra/tensor_product): characterise range of tensor product of two linear maps (#7340)

ocfnash committed 4 years ago

33ea6980

doc(field_theory/minpoly): improve some doc-strings (#7336)

kim-em committed 4 years ago

227c42d1

Newer Older