leanprover-community/mathlib3

Pull Requests Commits

chore(topology/metric_space): golf, generalize, rename (#6849)

urkud committed 4 years ago

d1044139

refactor(representation_theory/maschke): replaces `¬(ring_char k ∣ fintype.card G)` with `invertible (fintype.card G : k)` instance (#6901)

awainverse committed 4 years ago

cc7e722a

feat(data/nat/log): add some lemmas and monotonicity (#6899)

hallow-world committed 4 years ago

d32f9c72

feat(group_theory/order_of_element): order_of is the same in a submonoid (#6876)

tb65536 committed 4 years ago

5ecb1f73

awainverse committed 4 years ago

6cee0ce6

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

leanprover-community-bot committed 4 years ago

5c95d480

feat(algebra/module): pull-back module structures along homomorphisms (#6895)

eric-wieser committed 4 years ago

3fe67c86

chore(algebra/smul_with_zero): add missing injective / surjective transferring functions (#6892)

eric-wieser committed 4 years ago

4b261a86

refactor(topology/continuous_functions): change file layout (#6890)

kim-em committed 4 years ago

832a2eb9

refactor(analysis/normed_space/basic): add semi_normed_group (#6888)

riccardobrasca committed 4 years ago

99c23eaf

feat(group_theory/perm/cycles): is_cycle_of_is_cycle_pow (#6871)

tb65536 committed 4 years ago

bc33f1a9

feat(algebra/big_operators/basic): add lemmas for a product with two non one factors (#6826)

paulvanwamelen committed 4 years ago

5eead090

feat(linear_algebra/bilinear_form): generalize some constructions to the noncomm case (#6824)

hrmacbeth committed 4 years ago

cfd1a4cb

feat(order/lattice): add complete_semilattice_Sup/Inf (#6797)

kim-em committed 4 years ago

ec26d96a

awainverse committed 4 years ago

1d40e24e

chore(category_theory/monoidal): golf some proofs (#6894)

b-mehta committed 4 years ago

e36656ee

chore(data/equiv/transfer_instance): reuse existing proofs (#6868)

eric-wieser committed 4 years ago

e21b4bcb

feat(ring_theory/int/basic): Induction, nat_abs and units (#6733)

thejohncrafter committed 4 years ago

9e00c2bc

feat(geometry/manifold/algebra/smooth_functions): simp lemmas for coercions to functions (#6893)

ocfnash committed 4 years ago

ca7dca39

awainverse committed 4 years ago

b7e6b8fb

awainverse committed 4 years ago

e991521b

awainverse committed 4 years ago

8d699388

awainverse committed 4 years ago

bfd213b0

awainverse committed 4 years ago

9df68b7d

chore(algebra/group): rename `is_unit_unit` to `units.is_unit` (#6886)

urkud committed 4 years ago

902b01d8

chore(data/pi,algebra/group/pi): reorganize proofs (#6869)

urkud committed 4 years ago

e43d9649

feat(*): add more lemmas about `set.piecewise` (#6862)

urkud committed 4 years ago

3566cbba

feat(dynamics/ergodic/conservative): define conservative systems, formalize Poincaré recurrence thm (#2311)

urkud committed 4 years ago

ef7fe6f9

awainverse committed 4 years ago

6c07af44

awainverse committed 4 years ago

929260fd

Newer Older