Commits leanprover-community/mathlib3

more random things

alexjbest committed 3 years ago

ad3a3e0b

ok

alexjbest committed 3 years ago

5c1dd1f9

Merge branch 'master' of github.com:leanprover-community/mathlib into alexjbest/simple_edge_cases_linter

alexjbest committed 3 years ago

db9944c8

feat(group_theory/group_action/fixing_subgroup): add lemmas about fixing_subgroup (#13202)

AntoineChambert-Loir committed 3 years ago

9498beac

feat(category_theory/limits/terminal): limit of the constant terminal functor (#13238)

kim-em committed 3 years ago

ed266e51

feat(category_theory/limits/pullbacks): missing simp lemmas (#13237)

kim-em committed 3 years ago

afa9be28

feat(analysis/locally_convex/basic): add lemmas about finite unions for absorbs (#13236)

mcdoll committed 3 years ago

05213440

feat(data/polynomial/degree/definitions): add `degree_monoid_hom` (#13233)

astrainfinita committed 3 years ago

0831e4f1

feat(data/fintype/basic): add `fintype_of_{equiv,option}` (#13086)

stuart-presnell committed 3 years ago

f5d4fa19

feat(data/multiset/basic): add `map_le_map_iff` and `map_embedding` (#13082)

stuart-presnell committed 3 years ago

d96e17df

chore(computability/language): Golf (#13039)

YaelDillies committed 3 years ago

5acaeaf4

feat(data/set/intervals/basic): An open interval of a dense order has no maximum/minimum (#12924)

vihdzp committed 3 years ago

2569ad52

chore(model_theory/encoding): Move the encoding for terms to its own file (#13223)

awainverse committed 3 years ago

91ce04d4

feat(model_theory/*): Theory of nonempty structures and bundling elementary substructures (#13118)

awainverse committed 3 years ago

ed688546

feat(model_theory/order): Defines ordered languages and structures (#13088)

awainverse committed 3 years ago

710fe040

feat(group_theory/group_action/basic): Add typeclass for actions that descend to the quotient (#12999)

tb65536 committed 3 years ago

7340720c

feat(ring_theory/localization): b is linear independent over R iff l.i. over `Frac(R)` (#13041)

Vierkantor committed 3 years ago

851b3200

feat(archive/imo/imo2008_q3): golf (#13232)

hrmacbeth committed 3 years ago

7d417154

feat(group_theory/subgroup/basic): The centralizer of a characteristic subgroup is characteristic (#13230)

tb65536 committed 3 years ago

e85dc17a

refactor(group_theory/commutator): Move `commutator_le_map_commutator` (#13229)

tb65536 committed 3 years ago

95ebbadb

feat(group_theory/coset): Right cosets are in bijection with left cosets (#13228)

tb65536 committed 3 years ago

1a4203a9

feat(group_theory/index): `fintype_of_index_ne_zero` (#13225)

tb65536 committed 3 years ago

499a4a89

feat(ring_theory/unique_factorization_domain): alternative specification for `count (normalized_factors x)` (#13161)

Vierkantor committed 3 years ago

ccf3e37f

refactor(analysis/normed_space/conformal_linear_map): redefine (#13143)

urkud committed 3 years ago

0c424e95

feat(topology/uniform_space/uniform_convergence): add `tendsto_uniformly_iff_seq_tendsto_uniformly` (#13128)

kex-y committed 3 years ago

036fc996

feat(model_theory/basic,bundled): Structures induced by equivalences (#13124)

awainverse committed 3 years ago

ab60244a

feat(category_theory/limits): further API for commuting limits (#13215)

kim-em committed 3 years ago

9f3e7fba

feat(topology/continuous_function/zero_at_infty): add more instances for zero_at_infty_continuous_map and establish C₀ functorial properties (#13196)

j-loreaux committed 3 years ago

5e98dc1c

feat(category_theory/limits/shapes): isomorphisms of (co)spans (#13216)

kim-em committed 3 years ago

0719b36a

chore(algebra/associated): generalisation linter (#13108)

kim-em committed 3 years ago

b8971152