quotientBot — Mathlib

English

The canonical isomorphism between G/⊥ and G identifies the quotient by the trivial subgroup with G itself.

Русский

Канонический изоморфизм между G/⊥ и G идентифицирует фактор по тривиальной подгруппе с самим G.

LaTeX

$$G / (⊥) ≃* G$$

Lean4

/-- The canonical isomorphism `G/⊥ ≃* G`. -/
@[to_additive (attr := simps!) /-- The canonical isomorphism `G/⊥ ≃+ G`. -/
    ]
def quotientBot : G ⧸ (⊥ : Subgroup G) ≃* G :=
  quotientKerEquivOfRightInverse (MonoidHom.id G) id fun _x => rfl

Похожие утверждения