Mathlib Map

Theorems · Theorem · group theory

IsAddUnit.vadd_bijective

∀ {α : Type u_5} {β : Type u_6} [inst : AddMonoid α] [inst_1 : AddAction α β] {m : α},
  IsAddUnit m → Function.Bijective fun a => m +ᵥ a
Defined in
Mathlib.Algebra.Group.Action.Basic
Cited by
1 results in Mathlib
Foundations
Depth 22 from the axioms · uses propext, Quot.sound
Assumes
AddMonoidAddAction
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

preimage_vadd_setₛₗ_of_isAddUnit_isAddUnit · cited by 3preimage_vadd_setₛₗ_of_is…AddMonoid · cited by 2864AddMonoidHVAdd.hVAdd · cited by 1820HVAdd.hVAddFunction.Bijective · cited by 863Function.BijectiveAddAction · cited by 820AddActionAddUnits · cited by 325AddUnitsAddUnits.val · cited by 248AddUnits.valIsAddUnit · cited by 215IsAddUnitAddAction.bijective · cited by 6AddAction.bijectiveIsAddUnit.vadd_bijectiveCITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.