leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: general

Topic: lift (f \circ of) = f


Johan Commelin (Mar 05 2019 at 13:38):

How should I name this lemma?

@[simp] lemma lift'_of_comp (f : localization α S → β) [is_ring_hom f] :
  lift' (f ∘ of) (units.map f ∘ to_units) (λ s, rfl) = f :=

Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll